Theorem ad3antlr 490

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad3antlr	|- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad2antlr 486	. 2 |- ( ( ( ch /\ ph ) /\ th ) -> ps )
3	2	adantr 274	1 |- ( ( ( ( ch /\ ph ) /\ 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:  ad4antlr  492  nntr2  6482  phpm  6843  phplem4on  6845  fidifsnen  6848  fisbth  6861  fin0  6863  fin0or  6864  fiintim  6906  fisseneq  6909  djudom  7070  difinfsnlem  7076  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  prmuloc  7528  cauappcvgprlemopl  7608  cauappcvgprlemdisj  7613  cauappcvgprlemladdfl  7617  caucvgprlemopl  7631  axcaucvglemcau  7860  xnn0letri  9760  xaddf  9801  xleaddadd  9844  ssfzo12bi  10181  rebtwn2zlemstep  10209  btwnzge0  10256  addmodlteq  10354  frecuzrdgg  10372  qsqeqor  10586  apexp1  10652  hashxp  10761  cjap  10870  caucvgre  10945  minmax  11193  xrminmax  11228  sumeq2  11322  fsumconst  11417  ntrivcvgap  11511  prodeq2  11520  p1modz1  11756  bezoutlemmain  11953  dfgcd2  11969  uzwodc  11992  lcmgcdlem  12031  cnpnei  13013  cnntr  13019  txmetcnp  13312  lgsval  13699  pw1nct  14036  peano4nninf  14039