Theorem ad3antlr 484

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 480	. 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  486  nntr2  6399  phpm  6759  phplem4on  6761  fidifsnen  6764  fisbth  6777  fin0  6779  fin0or  6780  fiintim  6817  fisseneq  6820  djudom  6978  difinfsnlem  6984  enomnilem  7010  prmuloc  7374  cauappcvgprlemopl  7454  cauappcvgprlemdisj  7459  cauappcvgprlemladdfl  7463  caucvgprlemopl  7477  axcaucvglemcau  7706  xaddf  9627  xleaddadd  9670  ssfzo12bi  10002  rebtwn2zlemstep  10030  btwnzge0  10073  addmodlteq  10171  frecuzrdgg  10189  hashxp  10572  cjap  10678  caucvgre  10753  minmax  11001  xrminmax  11034  sumeq2  11128  fsumconst  11223  ntrivcvgap  11317  prodeq2  11326  bezoutlemmain  11686  dfgcd2  11702  lcmgcdlem  11758  cnpnei  12388  cnntr  12394  txmetcnp  12687  peano4nninf  13200  nninfalllemn  13202