ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3adant3 GIF version

Theorem 3adant3 924
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant3 ((𝜑𝜓𝜃) → 𝜒)

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 901 . 2 ((𝜑𝜓𝜃) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  stoic4a  1321  stoic4b  1322  vtoclgft  2604  eqeu  2711  tpssi  3530  issod  4056  sotricim  4060  soinxp  4410  funopg  4934  fnco  5007  resasplitss  5069  resdif  5148  fnimapr  5233  ftpg  5347  fsnunfv  5363  fvpr1g  5367  fvpr2g  5368  f1ocnvfvb  5420  f1oiso2  5466  moriotass  5496  f1ofveu  5500  acexmid  5511  ovig  5622  ov6g  5638  ovg  5639  ot1stg  5779  ot2ndg  5780  poxp  5853  brtposg  5869  smores3  5908  smoiso  5917  rdgivallem  5968  frecsuclemdm  5988  frecsuclem3  5990  nnaord  6082  nnaword  6084  nnawordex  6101  ecopovtrn  6203  ecopovtrng  6206  xpdom3m  6308  ltsopi  6418  addcanpig  6432  distrnqg  6485  ltsonq  6496  ltanqg  6498  ltmnqg  6499  nnanq0  6556  distrnq0  6557  distnq0r  6561  prarloclem  6599  genpassl  6622  genpassu  6623  distrlem1prl  6680  distrlem1pru  6681  distrlem5prl  6684  distrlem5pru  6685  1idprl  6688  1idpru  6689  ltpopr  6693  ltsopr  6694  ltexprlemm  6698  ltexprlemfl  6707  ltexprlemfu  6709  addcanprlemu  6713  recexprlem1ssl  6731  recexprlem1ssu  6732  aptipr  6739  lttrsr  6847  ltsosr  6849  ltasrg  6855  recexgt0sr  6858  mulextsr1  6865  axmulass  6947  ltxrlt  7085  axltwlin  7087  axlttrn  7088  axltadd  7089  letr  7101  mul12  7142  add12  7169  subadd  7214  addsub  7222  npncan  7232  nppcan  7233  nnpcan  7234  nppcan3  7235  pnpcan  7250  pnncan  7252  ppncan  7253  subdi  7382  ltaddsub2  7432  leaddsub2  7434  ltaddsublt  7562  apreap  7578  lemul1  7584  reapmul1lem  7585  reapadd1  7587  reapcotr  7589  receuap  7650  divassap  7669  div23ap  7670  divcanap4  7676  divsubdirap  7684  divcanap5  7690  divdiv32ap  7696  divdivap2  7700  letrp1  7814  ltmulgt12  7831  lediv1  7835  ltdiv2  7853  lediv2  7857  xrletr  8724  xrre2  8734  ixxdisj  8772  ubioc1  8798  lbico1  8799  elioo5  8802  iccsupr  8835  lbicc2  8852  ubicc2  8853  iccneg  8857  icoshft  8858  icodisj  8860  iccf1o  8872  fztri3or  8903  fzdcel  8904  fzen  8907  uzsubsubfz  8911  fzrevral2  8968  fzshftral  8970  fz0fzdiffz0  8987  elfzmlbmOLD  8989  difelfznle  8993  fzo1fzo0n0  9039  fzonmapblen  9043  fzosubel2  9051  ubmelfzo  9056  elfzodifsumelfzo  9057  ssfzo12bi  9081  ubmelm1fzo  9082  subfzo0  9097  ceiqle  9155  frec2uzf1od  9192  exprecap  9296  expdivap  9305  expubnd  9311  sqdivap  9318  bernneq2  9370  shftval2  9427  mulreap  9464  elicc4abs  9690  abssubge0  9698  abssuble0  9699
  Copyright terms: Public domain W3C validator