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  6714  phpm  7095  phplem4on  7097  fidifsnen  7100  fisbth  7115  fin0  7117  fin0or  7118  fiintim  7166  fisseneq  7170  djudom  7335  difinfsnlem  7341  nnnninfeq  7370  nnnninfeq2  7371  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  exmidapne  7522  prmuloc  7829  cauappcvgprlemopl  7909  cauappcvgprlemdisj  7914  cauappcvgprlemladdfl  7918  caucvgprlemopl  7932  axcaucvglemcau  8161  xnn0letri  10082  xaddf  10123  xleaddadd  10166  ssfzo12bi  10516  rebtwn2zlemstep  10558  btwnzge0  10606  addmodlteq  10706  frecuzrdgg  10724  qsqeqor  10958  apexp1  11026  hashxp  11136  ccatcl  11219  swrdccat3blem  11369  cjap  11529  caucvgre  11604  minmax  11853  xrminmax  11888  sumeq2  11982  fsumconst  12078  ntrivcvgap  12172  prodeq2  12181  p1modz1  12418  bezoutlemmain  12632  dfgcd2  12648  uzwodc  12671  nninfctlemfo  12674  lcmgcdlem  12712  4sqexercise2  13035  4sqlemsdc  13036  mulgval  13772  cnpnei  15013  cnntr  15019  txmetcnp  15312  mpomulcn  15360  lgsval  15806  upgriswlkdc  16284  pw1nct  16708  peano4nninf  16715