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

Theorem 3adant2 911
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 890 . 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:  3ad2ant1  913  eupickb  1963  vtoclegft  2602  eqeu  2688  suc11g  4219  soinxp  4337  funopg  4860  fnco  4933  dff1o2  5056  fnimapr  5158  fvun1  5164  fvmptt  5187  fnreseql  5202  fvpr1g  5292  fvpr2g  5293  f1elima  5337  f1ocnvfvb  5345  oprssov  5565  poxp  5775  smoiso  5839  rdgivallem  5888  nndi  5980  nndir  5984  nnaord  5993  nnaordr  5994  nnaword  5995  nnawordi  5999  ecopovtrn  6114  ecopovtrng  6117  ltsopi  6180  addcanpig  6194  addassnqg  6241  distrnqg  6246  ltsonq  6257  ltmnqg  6260  prarloclemarch2  6276  nnanq0  6313  distrnq0  6314  distnq0r  6318  prltlu  6341  prarloclem5  6354  distrlem1prl  6421  distrlem1pru  6422  distrlem5prl  6425  distrlem5pru  6426  ltpopr  6432  ltsopr  6433  ltexprlemm  6437  ltexprlemfl  6446  ltexprlemfu  6448  lttrsr  6509  ltsosr  6511  ltasrg  6517  recexsrlem  6520  adddir  6620  axltwlin  6688  axlttrn  6689  ltleletr  6698  letr  6699  nnncan1  6839  npncan3  6841  pnpcan2  6843  subdi  6974  subdir  6975  bj-peano4  7324
  Copyright terms: Public domain W3C validator