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

Theorem 3adant1 921
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((φ ψ) → χ)
Assertion
Ref Expression
3adant1 ((θ φ ψ) → χ)

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 902 . 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:  3ad2ant2  925  3ad2ant3  926  rsp2e  2366  sbciegft  2787  reuhyp  4170  suc11g  4235  soinxp  4353  breldmg  4484  funopg  4877  funimaexglem  4925  fex2  5002  fnreseql  5220  ftpg  5290  mpt2eq3ia  5512  mpt2fvex  5771  poxp  5794  smores3  5849  tfrlemibxssdm  5882  nndi  6004  nnmass  6005  nndir  6008  nnaord  6018  nnaordr  6019  nnawordi  6024  nnmord  6026  ecopovtrn  6139  ecopovtrng  6142  ltsopi  6304  addassnqg  6366  ltsonq  6382  ltmnqg  6385  distrnq0  6442  addlocpr  6519  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  ltpopr  6569  ltsopr  6570  addcanprg  6590  lttrsr  6690  ltsosr  6692  ltasrg  6698  recexgt0sr  6701  mulextsr1lem  6706  mulextsr1  6707  axpre-mulext  6772  adddir  6816  axltwlin  6884  axlttrn  6885  ltleletr  6897  letr  6898  mul32  6940  mul31  6941  add32  6967  subsub23  7013  addsubass  7018  subcan2  7032  subsub2  7035  nppcan2  7038  sub32  7041  nnncan  7042  nnncan2  7044  pnpcan2  7047  subdi  7178  subdir  7179  reapcotr  7382  receuap  7432  divmulap3  7438  divrecap  7449  divrecap2  7450  divsubdirap  7466  divdivap1  7481  redivclap  7489  div2negap  7493  ltmul2  7603  lemul2  7604  lemul2a  7606  lediv1  7616  gt0div  7617  ge0div  7618  ltdivmul  7623  ltdivmul2  7625  ledivmul2  7627  uzind2  8126  nn0ind  8128  fnn0ind  8130  uz3m2nn  8291  xrletr  8494  xrre2  8504  ixxdisj  8542  iooneg  8626  iccneg  8627  icoshft  8628  icoshftf1o  8629  icodisj  8630  fzen  8677  fzrev3  8719  2ffzeq  8768  fzoaddel2  8819  elfzodifsumelfzo  8827  ssfzo12bi  8851  fzoshftral  8864  frec2uzf1od  8873  expdivap  8959  mulreap  9092  bj-peano4  9415
  Copyright terms: Public domain W3C validator