Theorem ad3antlr 482

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 478	. 2 |- ( ( ( ch /\ ph ) /\ th ) -> ps )
3	2	adantr 272	1 |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4antlr  484  nntr2  6350  phpm  6709  phplem4on  6711  fidifsnen  6714  fisbth  6727  fin0  6729  fin0or  6730  fiintim  6767  fisseneq  6770  djudom  6927  difinfsnlem  6933  enomnilem  6957  prmuloc  7315  cauappcvgprlemopl  7395  cauappcvgprlemdisj  7400  cauappcvgprlemladdfl  7404  caucvgprlemopl  7418  axcaucvglemcau  7626  xaddf  9513  xleaddadd  9556  ssfzo12bi  9888  rebtwn2zlemstep  9916  btwnzge0  9959  addmodlteq  10057  frecuzrdgg  10075  hashxp  10458  cjap  10564  caucvgre  10638  minmax  10886  xrminmax  10919  sumeq2  11013  fsumconst  11108  bezoutlemmain  11525  dfgcd2  11541  lcmgcdlem  11597  cnpnei  12223  cnntr  12229  txmetcnp  12500  peano4nninf  12877  nninfalllemn  12879