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

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

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 911 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  3ad2ant1  934  eupickb  1995  vtoclegft  2640  eqeu  2731  suc11g  4306  soinxp  4435  funopg  4959  fnco  5032  dff1o2  5156  fnimapr  5258  fvun1  5264  fvmptt  5287  fnreseql  5302  fvpr1g  5392  fvpr2g  5393  f1elima  5437  f1ocnvfvb  5445  ovexg  5564  oprssov  5667  poxp  5878  smoiso  5945  rdgivallem  5996  nndi  6093  nndir  6097  nnaord  6110  nnaordr  6111  nnaword  6112  nnawordi  6116  ecopovtrn  6231  ecopovtrng  6234  xpdom3m  6336  findcard  6373  ltsopi  6446  addcanpig  6460  addassnqg  6508  distrnqg  6513  ltsonq  6524  ltmnqg  6527  prarloclemarch2  6545  nnanq0  6584  distrnq0  6585  distnq0r  6589  prltlu  6613  prarloclem5  6626  distrlem1prl  6708  distrlem1pru  6709  distrlem5prl  6712  distrlem5pru  6713  ltpopr  6721  ltsopr  6722  ltexprlemm  6726  ltexprlemfl  6735  ltexprlemfu  6737  lttrsr  6875  ltsosr  6877  ltasrg  6883  recexgt0sr  6886  mulextsr1lem  6892  mulextsr1  6893  axpre-mulext  6990  adddir  7046  axltwlin  7116  axlttrn  7117  ltleletr  7129  letr  7130  nnncan1  7280  npncan3  7282  pnpcan2  7284  subdi  7424  subdir  7425  reapcotr  7633  divmulap  7698  div23ap  7714  div13ap  7716  muldivdirap  7728  divsubdirap  7729  divcanap7  7742  ltmul2  7867  lemul2  7868  lemul2a  7870  lediv1  7880  ltmuldiv2  7886  lemuldiv2  7893  squeeze0  7915  nndivtr  8001  bndndx  8208  nn0n0n1ge2  8339  fnn0ind  8383  addlelt  8756  xrletr  8795  xrltne  8800  iooneg  8927  iccneg  8928  icoshft  8929  icoshftf1o  8930  zltaddlt1le  8945  fztri3or  8975  fzdcel  8976  fzen  8979  uzsubsubfz  8983  fzrevral2  9040  fzshftral  9042  fz0fzdiffz0  9059  elfzmlbmOLD  9061  elfzmlbp  9062  elfzo  9078  fzoaddel2  9121  fzosubel2  9123  elfzom1p1elfzo  9142  ssfzo12bi  9153  subfzo0  9169  flltdivnn0lt  9219  modqmulnn  9257  modfzo0difsn  9310  expdivap  9436  expubnd  9442  mulbinom2  9497  bernneq2  9502  shftuz  9610  shftval2  9619  abs3dif  9895  dvdsval2  10074  dvdscmul  10097  dvdsmulc  10098  bj-peano4  10410
  Copyright terms: Public domain W3C validator