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

Theorem ad3antrrr 483
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antrrr  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 274 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 479 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
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  disjiun  3894  tfr1onlemaccex  6213  tfrcllemaccex  6226  phplem4on  6729  dif1enen  6742  en2eqpr  6769  unsnfidcex  6776  unsnfidcel  6777  unfidisj  6778  undifdc  6780  fiintim  6785  ssfirab  6790  suplub2ti  6856  djudom  6946  omp1eomlem  6947  difinfsnlem  6952  difinfinf  6954  ctssdclemn0  6963  ctssdc  6966  ltaddpr  7373  ltexprlemrl  7386  addcanprleml  7390  addcanprlemu  7391  aptiprleml  7415  aptiprlemu  7416  cauappcvgprlemdisj  7427  cauappcvgprlemladdrl  7433  caucvgprlemloc  7451  caucvgprlemladdrl  7454  caucvgprprlemopl  7473  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  suplocexprlemrl  7493  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  caucvgsrlemoffres  7576  suplocsrlem  7584  axcaucvglemcau  7674  axcaucvglemres  7675  negf1o  8112  apreim  8332  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  mulge0  8348  apti  8351  aprcl  8375  qapne  9387  xaddf  9582  xaddval  9583  qtri3or  9975  exbtwnzlemstep  9980  rebtwn2zlemstep  9985  addmodlteq  10126  seq3f1olemqsumk  10227  seq3f1oleml  10231  faclbnd  10442  hashennnuni  10480  cvg1nlemres  10712  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemga  10750  minmax  10956  xrmaxleim  10968  xrmaxifle  10970  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxiflemcom  10973  xrmaxltsup  10982  xrmaxadd  10985  xrminmax  10989  xrbdtri  11000  climrecvg1n  11072  serf0  11076  zsumdc  11108  isumss  11115  fisumss  11116  fsum3cvg3  11120  fsumcl2lem  11122  fsumadd  11130  fsummulc2  11172  divcnv  11221  cvgratz  11256  mertenslem2  11260  dvds2ln  11438  divalglemeunn  11530  divalglemeuneg  11532  zsupcllemstep  11550  dvdsbnd  11557  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlembi  11605  dfgcd3  11610  lcmgcdlem  11670  cncongr1  11696  cncongr2  11697  ennnfonelemhom  11839  ennnfonelemrnh  11840  ctinfomlemom  11851  cnpnei  12299  cnntr  12305  cncnp  12310  lmtopcnp  12330  txdis1cn  12358  xmettxlem  12589  metcnp3  12591  fsumcncntop  12636  cncfco  12658  mulcncf  12671  dedekindeulemuub  12675  dedekindeulemlu  12679  dedekindicclemuub  12684  dedekindicclemlu  12688  dedekindicclemicc  12690  ivthinclemlr  12695  ivthinclemur  12697  limcimo  12714  cnplimcim  12716  pilem3  12775  peano4nninf  13096  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator