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

Theorem ad3antrrr 492
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 276 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 488 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  ad4antr  494  ad5ant12  518  disjiun  3995  tfr1onlemaccex  6342  tfrcllemaccex  6355  phplem4on  6860  dif1enen  6873  en2eqpr  6900  unsnfidcex  6912  unsnfidcel  6913  unfidisj  6914  undifdc  6916  fiintim  6921  ssfirab  6926  suplub2ti  6993  djudom  7085  omp1eomlem  7086  difinfsnlem  7091  difinfinf  7093  ctssdclemn0  7102  ctssdc  7105  nnnninfeq2  7120  nninfisol  7124  nninfwlpoimlemginf  7167  cc3  7245  ltaddpr  7574  ltexprlemrl  7587  addcanprleml  7591  addcanprlemu  7592  aptiprleml  7616  aptiprlemu  7617  cauappcvgprlemdisj  7628  cauappcvgprlemladdrl  7634  caucvgprlemloc  7652  caucvgprlemladdrl  7655  caucvgprprlemopl  7674  caucvgprprlemloc  7680  caucvgprprlemexbt  7683  suplocexprlemrl  7694  suplocexprlemru  7696  suplocexprlemdisj  7697  suplocexprlemloc  7698  suplocexprlemub  7700  caucvgsrlemoffres  7777  suplocsrlem  7785  axcaucvglemcau  7875  axcaucvglemres  7876  negf1o  8316  apreim  8537  apsym  8540  apcotr  8541  apadd1  8542  apneg  8545  mulext1  8546  mulge0  8553  apti  8556  aprcl  8580  qapne  9615  xaddf  9818  xaddval  9819  qtri3or  10216  exbtwnzlemstep  10221  rebtwn2zlemstep  10226  addmodlteq  10371  seq3f1olemqsumk  10472  seq3f1oleml  10476  qsqeqor  10603  apexp1  10669  faclbnd  10692  hashennnuni  10730  cvg1nlemres  10965  resqrexlemoverl  11001  resqrexlemglsq  11002  resqrexlemga  11003  minmax  11209  xrmaxleim  11223  xrmaxifle  11225  xrmaxiflemab  11226  xrmaxiflemlub  11227  xrmaxiflemcom  11228  xrmaxltsup  11237  xrmaxadd  11240  xrminmax  11244  xrbdtri  11255  climrecvg1n  11327  serf0  11331  zsumdc  11363  isumss  11370  fisumss  11371  fsum3cvg3  11375  fsumcl2lem  11377  fsumadd  11385  fsummulc2  11427  divcnv  11476  cvgratz  11511  mertenslem2  11515  zproddc  11558  fprodssdc  11569  fprodmul  11570  fprodsplitdc  11575  fprodcl2lem  11584  fprodle  11619  fprodmodd  11620  p1modz1  11772  dvds2ln  11802  divalglemeunn  11896  divalglemeuneg  11898  zsupcllemstep  11916  dvdsbnd  11927  bezoutlemnewy  11967  bezoutlemstep  11968  bezoutlemmain  11969  bezoutlembi  11976  dfgcd3  11981  uzwodc  12008  lcmgcdlem  12047  cncongr1  12073  cncongr2  12074  isprm5  12112  odzdvds  12215  pclemdc  12258  pceu  12265  dvdsprmpweqle  12306  pcadd  12309  1arith  12335  ennnfonelemhom  12386  ennnfonelemrnh  12387  ctinfomlemom  12398  mhmid  12855  mhmmnd  12856  ghmgrp  12858  mulgfng  12863  issrg  12961  ringinvnzdiv  13040  cnpnei  13352  cnntr  13358  cncnp  13363  lmtopcnp  13383  txdis1cn  13411  xmettxlem  13642  metcnp3  13644  fsumcncntop  13689  cncfco  13711  mulcncf  13724  dedekindeulemuub  13728  dedekindeulemlu  13732  dedekindicclemuub  13737  dedekindicclemlu  13741  dedekindicclemicc  13743  ivthinclemlr  13748  ivthinclemur  13750  limcimo  13767  cnplimcim  13769  pilem3  13837  lgsfcl2  14040  lgsval2lem  14044  lgsdir  14069  lgsne0  14072  peano4nninf  14378  trilpolemeq1  14411
  Copyright terms: Public domain W3C validator