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

Theorem 3adant1 910
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 891 . 2 ((θ φ ψ) → (φ ψ))
2 3adant.1 . 2 ((φ ψ) → χ)
31, 2syl 14 1 ((θ φ ψ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
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 875
This theorem is referenced by:  3ad2ant2  914  3ad2ant3  915  rsp2e  2350  sbciegft  2770  reuhyp  4154  suc11g  4219  soinxp  4337  breldmg  4468  funopg  4860  funimaexglem  4908  fex2  4984  fnreseql  5202  ftpg  5272  mpt2eq3ia  5493  mpt2fvex  5752  poxp  5775  smores3  5830  tfrlemibxssdm  5862  nndi  5980  nnmass  5981  nndir  5984  nnaord  5993  nnaordr  5994  nnawordi  5999  nnmord  6001  ecopovtrn  6114  ecopovtrng  6117  ltsopi  6180  addassnqg  6241  ltsonq  6257  ltmnqg  6260  distrnq0  6314  addlocpr  6391  distrlem1prl  6421  distrlem1pru  6422  distrlem4prl  6423  distrlem4pru  6424  ltpopr  6432  ltsopr  6433  addcanprg  6453  lttrsr  6509  ltsosr  6511  ltasrg  6517  recexsrlem  6520  adddir  6620  axltwlin  6688  axlttrn  6689  ltleletr  6698  letr  6699  mul32  6730  mul31  6731  add32  6757  subsub23  6803  addsubass  6808  subcan2  6822  subsub2  6825  nppcan2  6828  sub32  6831  nnncan  6832  nnncan2  6834  pnpcan2  6837  subdi  6968  subdir  6969  bj-peano4  7177
  Copyright terms: Public domain W3C validator