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

Theorem ad3antrrr 483
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 274 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 479 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad4antr  485  ad5ant12  509  disjiun  3924  tfr1onlemaccex  6245  tfrcllemaccex  6258  phplem4on  6761  dif1enen  6774  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  unfidisj  6810  undifdc  6812  fiintim  6817  ssfirab  6822  suplub2ti  6888  djudom  6978  omp1eomlem  6979  difinfsnlem  6984  difinfinf  6986  ctssdclemn0  6995  ctssdc  6998  cc3  7088  ltaddpr  7417  ltexprlemrl  7430  addcanprleml  7434  addcanprlemu  7435  aptiprleml  7459  aptiprlemu  7460  cauappcvgprlemdisj  7471  cauappcvgprlemladdrl  7477  caucvgprlemloc  7495  caucvgprlemladdrl  7498  caucvgprprlemopl  7517  caucvgprprlemloc  7523  caucvgprprlemexbt  7526  suplocexprlemrl  7537  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  caucvgsrlemoffres  7620  suplocsrlem  7628  axcaucvglemcau  7718  axcaucvglemres  7719  negf1o  8156  apreim  8377  apsym  8380  apcotr  8381  apadd1  8382  apneg  8385  mulext1  8386  mulge0  8393  apti  8396  aprcl  8420  qapne  9443  xaddf  9639  xaddval  9640  qtri3or  10032  exbtwnzlemstep  10037  rebtwn2zlemstep  10042  addmodlteq  10183  seq3f1olemqsumk  10284  seq3f1oleml  10288  faclbnd  10499  hashennnuni  10537  cvg1nlemres  10769  resqrexlemoverl  10805  resqrexlemglsq  10806  resqrexlemga  10807  minmax  11013  xrmaxleim  11025  xrmaxifle  11027  xrmaxiflemab  11028  xrmaxiflemlub  11029  xrmaxiflemcom  11030  xrmaxltsup  11039  xrmaxadd  11042  xrminmax  11046  xrbdtri  11057  climrecvg1n  11129  serf0  11133  zsumdc  11165  isumss  11172  fisumss  11173  fsum3cvg3  11177  fsumcl2lem  11179  fsumadd  11187  fsummulc2  11229  divcnv  11278  cvgratz  11313  mertenslem2  11317  dvds2ln  11537  divalglemeunn  11629  divalglemeuneg  11631  zsupcllemstep  11649  dvdsbnd  11656  bezoutlemnewy  11695  bezoutlemstep  11696  bezoutlemmain  11697  bezoutlembi  11704  dfgcd3  11709  lcmgcdlem  11769  cncongr1  11795  cncongr2  11796  ennnfonelemhom  11939  ennnfonelemrnh  11940  ctinfomlemom  11951  cnpnei  12402  cnntr  12408  cncnp  12413  lmtopcnp  12433  txdis1cn  12461  xmettxlem  12692  metcnp3  12694  fsumcncntop  12739  cncfco  12761  mulcncf  12774  dedekindeulemuub  12778  dedekindeulemlu  12782  dedekindicclemuub  12787  dedekindicclemlu  12791  dedekindicclemicc  12793  ivthinclemlr  12798  ivthinclemur  12800  limcimo  12817  cnplimcim  12819  pilem3  12886  peano4nninf  13261  trilpolemeq1  13294
  Copyright terms: Public domain W3C validator