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

Theorem ad3antrrr 476
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antrrr ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 270 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 472 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad4antr  478  tfr1onlemaccex  6061  tfrcllemaccex  6074  phplem4on  6529  dif1enen  6542  en2eqpr  6569  unsnfidcex  6576  unsnfidcel  6577  unfidisj  6578  undifdc  6580  ssfirab  6587  suplub2ti  6633  djudom  6724  ltaddpr  7093  ltexprlemrl  7106  addcanprleml  7110  addcanprlemu  7111  aptiprleml  7135  aptiprlemu  7136  cauappcvgprlemdisj  7147  cauappcvgprlemladdrl  7153  caucvgprlemloc  7171  caucvgprlemladdrl  7174  caucvgprprlemopl  7193  caucvgprprlemloc  7199  caucvgprprlemexbt  7202  caucvgsrlemoffres  7282  axcaucvglemcau  7370  axcaucvglemres  7371  negf1o  7797  apreim  8014  apsym  8017  apcotr  8018  apadd1  8019  apneg  8022  mulext1  8023  mulge0  8030  apti  8033  qapne  9049  qtri3or  9575  exbtwnzlemstep  9580  rebtwn2zlemstep  9585  addmodlteq  9726  iseqf1olemqsumk  9825  iseqf1oleml  9829  faclbnd  10038  hashennnuni  10076  cvg1nlemres  10306  resqrexlemoverl  10342  resqrexlemglsq  10343  resqrexlemga  10344  minmax  10547  climrecvg1n  10620  serif0  10624  zisum  10656  isumss  10662  dvds2ln  10696  divalglemeunn  10788  divalglemeuneg  10790  zsupcllemstep  10808  dvdsbnd  10815  bezoutlemnewy  10852  bezoutlemstep  10853  bezoutlemmain  10854  bezoutlembi  10861  dfgcd3  10866  lcmgcdlem  10926  cncongr1  10952  cncongr2  10953  peano4nninf  11326
  Copyright terms: Public domain W3C validator