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

Theorem ad3antrrr 481
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 272 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 477 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  483  disjiun  3892  tfr1onlemaccex  6211  tfrcllemaccex  6224  phplem4on  6727  dif1enen  6740  en2eqpr  6767  unsnfidcex  6774  unsnfidcel  6775  unfidisj  6776  undifdc  6778  fiintim  6783  ssfirab  6788  suplub2ti  6854  djudom  6944  omp1eomlem  6945  difinfsnlem  6950  difinfinf  6952  ctssdclemn0  6961  ctssdc  6964  ltaddpr  7369  ltexprlemrl  7382  addcanprleml  7386  addcanprlemu  7387  aptiprleml  7411  aptiprlemu  7412  cauappcvgprlemdisj  7423  cauappcvgprlemladdrl  7429  caucvgprlemloc  7447  caucvgprlemladdrl  7450  caucvgprprlemopl  7469  caucvgprprlemloc  7475  caucvgprprlemexbt  7478  suplocexprlemrl  7489  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  caucvgsrlemoffres  7572  suplocsrlem  7580  axcaucvglemcau  7670  axcaucvglemres  7671  negf1o  8108  apreim  8328  apsym  8331  apcotr  8332  apadd1  8333  apneg  8336  mulext1  8337  mulge0  8344  apti  8347  aprcl  8370  qapne  9380  xaddf  9567  xaddval  9568  qtri3or  9960  exbtwnzlemstep  9965  rebtwn2zlemstep  9970  addmodlteq  10111  seq3f1olemqsumk  10212  seq3f1oleml  10216  faclbnd  10427  hashennnuni  10465  cvg1nlemres  10697  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemga  10735  minmax  10941  xrmaxleim  10953  xrmaxifle  10955  xrmaxiflemab  10956  xrmaxiflemlub  10957  xrmaxiflemcom  10958  xrmaxltsup  10967  xrmaxadd  10970  xrminmax  10974  xrbdtri  10985  climrecvg1n  11057  serf0  11061  zsumdc  11093  isumss  11100  fisumss  11101  fsum3cvg3  11105  fsumcl2lem  11107  fsumadd  11115  fsummulc2  11157  divcnv  11206  cvgratz  11241  mertenslem2  11245  dvds2ln  11422  divalglemeunn  11514  divalglemeuneg  11516  zsupcllemstep  11534  dvdsbnd  11541  bezoutlemnewy  11580  bezoutlemstep  11581  bezoutlemmain  11582  bezoutlembi  11589  dfgcd3  11594  lcmgcdlem  11654  cncongr1  11680  cncongr2  11681  ennnfonelemhom  11823  ennnfonelemrnh  11824  ctinfomlemom  11835  cnpnei  12283  cnntr  12289  cncnp  12294  lmtopcnp  12314  txdis1cn  12342  xmettxlem  12573  metcnp3  12575  fsumcncntop  12620  cncfco  12642  mulcncf  12655  dedekindeulemuub  12659  dedekindeulemlu  12663  limcimo  12677  cnplimcim  12679  peano4nninf  13002  trilpolemeq1  13035
  Copyright terms: Public domain W3C validator