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  6045  tfrcllemaccex  6058  phplem4on  6513  dif1enen  6526  en2eqpr  6550  unsnfidcex  6557  unsnfidcel  6558  unfidisj  6559  undifdc  6561  ssfirab  6568  suplub2ti  6603  djudom  6694  ltaddpr  7059  ltexprlemrl  7072  addcanprleml  7076  addcanprlemu  7077  aptiprleml  7101  aptiprlemu  7102  cauappcvgprlemdisj  7113  cauappcvgprlemladdrl  7119  caucvgprlemloc  7137  caucvgprlemladdrl  7140  caucvgprprlemopl  7159  caucvgprprlemloc  7165  caucvgprprlemexbt  7168  caucvgsrlemoffres  7248  axcaucvglemcau  7336  axcaucvglemres  7337  negf1o  7763  apreim  7980  apsym  7983  apcotr  7984  apadd1  7985  apneg  7988  mulext1  7989  mulge0  7996  apti  7999  qapne  9019  qtri3or  9543  exbtwnzlemstep  9548  rebtwn2zlemstep  9553  addmodlteq  9694  faclbnd  9984  hashennnuni  10022  cvg1nlemres  10245  resqrexlemoverl  10281  resqrexlemglsq  10282  resqrexlemga  10283  minmax  10486  climrecvg1n  10559  serif0  10563  dvds2ln  10609  divalglemeunn  10701  divalglemeuneg  10703  zsupcllemstep  10721  dvdsbnd  10728  bezoutlemnewy  10765  bezoutlemstep  10766  bezoutlemmain  10767  bezoutlembi  10774  dfgcd3  10779  lcmgcdlem  10839  cncongr1  10865  cncongr2  10866
  Copyright terms: Public domain W3C validator