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  6647  phpm  7023  phplem4on  7025  fidifsnen  7028  fisbth  7041  fin0  7043  fin0or  7044  fiintim  7089  fisseneq  7092  djudom  7256  difinfsnlem  7262  nnnninfeq  7291  nnnninfeq2  7292  enomnilem  7301  enmkvlem  7324  enwomnilem  7332  exmidapne  7442  prmuloc  7749  cauappcvgprlemopl  7829  cauappcvgprlemdisj  7834  cauappcvgprlemladdfl  7838  caucvgprlemopl  7852  axcaucvglemcau  8081  xnn0letri  9995  xaddf  10036  xleaddadd  10079  ssfzo12bi  10426  rebtwn2zlemstep  10467  btwnzge0  10515  addmodlteq  10615  frecuzrdgg  10633  qsqeqor  10867  apexp1  10935  hashxp  11043  ccatcl  11123  swrdccat3blem  11266  cjap  11412  caucvgre  11487  minmax  11736  xrminmax  11771  sumeq2  11865  fsumconst  11960  ntrivcvgap  12054  prodeq2  12063  p1modz1  12300  bezoutlemmain  12514  dfgcd2  12530  uzwodc  12553  nninfctlemfo  12556  lcmgcdlem  12594  4sqexercise2  12917  4sqlemsdc  12918  mulgval  13654  cnpnei  14887  cnntr  14893  txmetcnp  15186  mpomulcn  15234  lgsval  15677  pw1nct  16328  peano4nninf  16331