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

Theorem 3adant3 935
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 912 . 2 ((𝜑𝜓𝜃) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  stoic4a  1337  stoic4b  1338  vtoclgft  2621  eqeu  2733  tpssi  3557  issod  4083  sotricim  4087  soinxp  4437  funopg  4961  fnco  5034  resasplitss  5096  resdif  5175  fnimapr  5260  ftpg  5374  fsnunfv  5390  fvpr1g  5394  fvpr2g  5395  f1ocnvfvb  5447  f1oiso2  5493  moriotass  5523  f1ofveu  5527  acexmid  5538  ovig  5649  ov6g  5665  ovg  5666  ot1stg  5806  ot2ndg  5807  poxp  5880  brtposg  5899  smores3  5938  smoiso  5947  rdgivallem  5998  frecsuclemdm  6018  frecsuclem3  6020  nnaord  6112  nnaword  6114  nnawordex  6131  ecopovtrn  6233  ecopovtrng  6236  xpdom3m  6338  ltsopi  6475  addcanpig  6489  distrnqg  6542  ltsonq  6553  ltanqg  6555  ltmnqg  6556  nnanq0  6613  distrnq0  6614  distnq0r  6618  prarloclem  6656  genpassl  6679  genpassu  6680  distrlem1prl  6737  distrlem1pru  6738  distrlem5prl  6741  distrlem5pru  6742  1idprl  6745  1idpru  6746  ltpopr  6750  ltsopr  6751  ltexprlemm  6755  ltexprlemfl  6764  ltexprlemfu  6766  addcanprlemu  6770  recexprlem1ssl  6788  recexprlem1ssu  6789  aptipr  6796  lttrsr  6904  ltsosr  6906  ltasrg  6912  recexgt0sr  6915  mulextsr1  6922  axmulass  7004  ltxrlt  7143  axltwlin  7145  axlttrn  7146  axltadd  7147  letr  7159  mul12  7202  add12  7231  subadd  7276  addsub  7284  npncan  7294  nppcan  7295  nnpcan  7296  nppcan3  7297  pnpcan  7312  pnncan  7314  ppncan  7315  subdi  7453  ltaddsub2  7505  leaddsub2  7507  ltaddsublt  7635  apreap  7651  lemul1  7657  reapmul1lem  7658  reapadd1  7660  reapcotr  7662  receuap  7723  divassap  7742  div23ap  7743  divcanap4  7749  divsubdirap  7758  divcanap5  7764  divdiv32ap  7770  divdivap2  7774  letrp1  7888  ltmulgt12  7905  lediv1  7909  ltdiv2  7927  lediv2  7931  xrletr  8824  xrre2  8834  ixxdisj  8872  ubioc1  8898  lbico1  8899  elioo5  8902  iccsupr  8935  lbicc2  8952  ubicc2  8953  iccneg  8957  icoshft  8958  icodisj  8960  iccf1o  8972  zltaddlt1le  8974  fztri3or  9004  fzdcel  9005  fzen  9008  uzsubsubfz  9012  fzrevral2  9069  fzshftral  9071  fz0fzdiffz0  9088  elfzmlbmOLD  9090  difelfznle  9094  fzo1fzo0n0  9140  fzonmapblen  9144  fzosubel2  9152  ubmelfzo  9157  elfzodifsumelfzo  9158  ssfzo12bi  9182  ubmelm1fzo  9183  subfzo0  9198  ceiqle  9262  modqid2  9300  zmodidfzoimp  9303  addmodidr  9322  modfzo0difsn  9344  addmodlteq  9347  frec2uzf1od  9355  exprecap  9460  expdivap  9470  expubnd  9476  sqdivap  9483  mulbinom2  9532  bernneq2  9537  bcval3  9618  bccmpl  9621  shftval2  9654  mulreap  9691  elicc4abs  9920  abssubge0  9928  abssuble0  9929  dvdscmul  10133  summodnegmod  10137  modmulconst  10138  dvdsleabs  10156  dvdsleabs2  10157  addmodlteqALT  10170  dvdsexp  10172  mulmoddvds  10174
  Copyright terms: Public domain W3C validator