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  6556  distrlem1pru  6557  distrlem5prl  6560  distrlem5pru  6561  ltpopr  6567  ltsopr  6568  ltexprlemm  6572  ltexprlemfl  6581  ltexprlemfu  6583  lttrsr  6650  ltsosr  6652  ltasrg  6658  recexgt0sr  6661  mulextsr1lem  6666  mulextsr1  6667  axpre-mulext  6732  adddir  6776  axltwlin  6844  axlttrn  6845  ltleletr  6857  letr  6858  nnncan1  7003  npncan3  7005  pnpcan2  7007  subdi  7138  subdir  7139  reapcotr  7342  divmulap  7396  div23ap  7412  div13ap  7414  divsubdirap  7426  divcanap7  7439  ltmul2  7563  lemul2  7564  lemul2a  7566  lediv1  7576  ltmuldiv2  7582  lemuldiv2  7589  squeeze0  7611  nndivtr  7696  bndndx  7916  nn0n0n1ge2  8047  fnn0ind  8090  xrletr  8454  xrltne  8459  iooneg  8586  iccneg  8587  icoshft  8588  icoshftf1o  8589  fztri3or  8633  fzdcel  8634  fzen  8637  uzsubsubfz  8641  fzrevral2  8698  fzshftral  8700  fz0fzdiffz0  8717  elfzmlbmOLD  8719  elfzmlbp  8720  elfzo  8736  fzoaddel2  8779  fzosubel2  8781  elfzom1p1elfzo  8800  ssfzo12bi  8811  expdivap  8919  expubnd  8925  bernneq2  8983  bj-peano4  9343
  Copyright terms: Public domain W3C validator