Theorem ad3antlr 493

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

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:  ad4antlr  495  nntr2  6670  phpm  7051  phplem4on  7053  fidifsnen  7056  fisbth  7071  fin0  7073  fin0or  7074  fiintim  7122  fisseneq  7126  djudom  7291  difinfsnlem  7297  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  exmidapne  7478  prmuloc  7785  cauappcvgprlemopl  7865  cauappcvgprlemdisj  7870  cauappcvgprlemladdfl  7874  caucvgprlemopl  7888  axcaucvglemcau  8117  xnn0letri  10037  xaddf  10078  xleaddadd  10121  ssfzo12bi  10469  rebtwn2zlemstep  10511  btwnzge0  10559  addmodlteq  10659  frecuzrdgg  10677  qsqeqor  10911  apexp1  10979  hashxp  11089  ccatcl  11169  swrdccat3blem  11319  cjap  11466  caucvgre  11541  minmax  11790  xrminmax  11825  sumeq2  11919  fsumconst  12014  ntrivcvgap  12108  prodeq2  12117  p1modz1  12354  bezoutlemmain  12568  dfgcd2  12584  uzwodc  12607  nninfctlemfo  12610  lcmgcdlem  12648  4sqexercise2  12971  4sqlemsdc  12972  mulgval  13708  cnpnei  14942  cnntr  14948  txmetcnp  15241  mpomulcn  15289  lgsval  15732  upgriswlkdc  16210  pw1nct  16604  peano4nninf  16608