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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 274	. 2 |- ( ( ph /\ ch ) -> ps )
3	2	ad2antrr 479	1 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

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  3919  tfr1onlemaccex  6238  tfrcllemaccex  6251  phplem4on  6754  dif1enen  6767  en2eqpr  6794  unsnfidcex  6801  unsnfidcel  6802  unfidisj  6803  undifdc  6805  fiintim  6810  ssfirab  6815  suplub2ti  6881  djudom  6971  omp1eomlem  6972  difinfsnlem  6977  difinfinf  6979  ctssdclemn0  6988  ctssdc  6991  ltaddpr  7398  ltexprlemrl  7411  addcanprleml  7415  addcanprlemu  7416  aptiprleml  7440  aptiprlemu  7441  cauappcvgprlemdisj  7452  cauappcvgprlemladdrl  7458  caucvgprlemloc  7476  caucvgprlemladdrl  7479  caucvgprprlemopl  7498  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  suplocexprlemrl  7518  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  caucvgsrlemoffres  7601  suplocsrlem  7609  axcaucvglemcau  7699  axcaucvglemres  7700  negf1o  8137  apreim  8358  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  mulge0  8374  apti  8377  aprcl  8401  qapne  9424  xaddf  9620  xaddval  9621  qtri3or  10013  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  addmodlteq  10164  seq3f1olemqsumk  10265  seq3f1oleml  10269  faclbnd  10480  hashennnuni  10518  cvg1nlemres  10750  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemga  10788  minmax  10994  xrmaxleim  11006  xrmaxifle  11008  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxiflemcom  11011  xrmaxltsup  11020  xrmaxadd  11023  xrminmax  11027  xrbdtri  11038  climrecvg1n  11110  serf0  11114  zsumdc  11146  isumss  11153  fisumss  11154  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  fsummulc2  11210  divcnv  11259  cvgratz  11294  mertenslem2  11298  dvds2ln  11515  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  dvdsbnd  11634  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlembi  11682  dfgcd3  11687  lcmgcdlem  11747  cncongr1  11773  cncongr2  11774  ennnfonelemhom  11917  ennnfonelemrnh  11918  ctinfomlemom  11929  cnpnei  12377  cnntr  12383  cncnp  12388  lmtopcnp  12408  txdis1cn  12436  xmettxlem  12667  metcnp3  12669  fsumcncntop  12714  cncfco  12736  mulcncf  12749  dedekindeulemuub  12753  dedekindeulemlu  12757  dedekindicclemuub  12762  dedekindicclemlu  12766  dedekindicclemicc  12768  ivthinclemlr  12773  ivthinclemur  12775  limcimo  12792  cnplimcim  12794  pilem3  12853  peano4nninf  13189  trilpolemeq1  13222