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

Theorem 3adant2 922
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 901 . 2 ((φ θ ψ) → (φ ψ))
2 3adant.1 . 2 ((φ ψ) → χ)
31, 2syl 14 1 ((φ θ ψ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3ad2ant1  924  eupickb  1978  vtoclegft  2619  eqeu  2705  suc11g  4235  soinxp  4353  funopg  4877  fnco  4950  dff1o2  5074  fnimapr  5176  fvun1  5182  fvmptt  5205  fnreseql  5220  fvpr1g  5310  fvpr2g  5311  f1elima  5355  f1ocnvfvb  5363  oprssov  5584  poxp  5794  smoiso  5858  rdgivallem  5908  nndi  6004  nndir  6008  nnaord  6018  nnaordr  6019  nnaword  6020  nnawordi  6024  ecopovtrn  6139  ecopovtrng  6142  xpdom3m  6244  ltsopi  6304  addcanpig  6318  addassnqg  6366  distrnqg  6371  ltsonq  6382  ltmnqg  6385  prarloclemarch2  6402  nnanq0  6440  distrnq0  6441  distnq0r  6445  prltlu  6469  prarloclem5  6482  distrlem1prl  6557  distrlem1pru  6558  distrlem5prl  6561  distrlem5pru  6562  ltpopr  6568  ltsopr  6569  ltexprlemm  6573  ltexprlemfl  6582  ltexprlemfu  6584  lttrsr  6670  ltsosr  6672  ltasrg  6678  recexgt0sr  6681  mulextsr1lem  6686  mulextsr1  6687  axpre-mulext  6752  adddir  6796  axltwlin  6864  axlttrn  6865  ltleletr  6877  letr  6878  nnncan1  7023  npncan3  7025  pnpcan2  7027  subdi  7158  subdir  7159  reapcotr  7362  divmulap  7416  div23ap  7432  div13ap  7434  divsubdirap  7446  divcanap7  7459  ltmul2  7583  lemul2  7584  lemul2a  7586  lediv1  7596  ltmuldiv2  7602  lemuldiv2  7609  squeeze0  7631  nndivtr  7716  bndndx  7936  nn0n0n1ge2  8067  fnn0ind  8110  xrletr  8474  xrltne  8479  iooneg  8606  iccneg  8607  icoshft  8608  icoshftf1o  8609  fztri3or  8653  fzdcel  8654  fzen  8657  uzsubsubfz  8661  fzrevral2  8718  fzshftral  8720  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  elfzo  8756  fzoaddel2  8799  fzosubel2  8801  elfzom1p1elfzo  8820  ssfzo12bi  8831  expdivap  8939  expubnd  8945  bernneq2  9003  bj-peano4  9389
  Copyright terms: Public domain W3C validator