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  6666  phpm  7047  phplem4on  7049  fidifsnen  7052  fisbth  7065  fin0  7067  fin0or  7068  fiintim  7116  fisseneq  7119  djudom  7283  difinfsnlem  7289  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  exmidapne  7469  prmuloc  7776  cauappcvgprlemopl  7856  cauappcvgprlemdisj  7861  cauappcvgprlemladdfl  7865  caucvgprlemopl  7879  axcaucvglemcau  8108  xnn0letri  10028  xaddf  10069  xleaddadd  10112  ssfzo12bi  10460  rebtwn2zlemstep  10502  btwnzge0  10550  addmodlteq  10650  frecuzrdgg  10668  qsqeqor  10902  apexp1  10970  hashxp  11080  ccatcl  11160  swrdccat3blem  11310  cjap  11457  caucvgre  11532  minmax  11781  xrminmax  11816  sumeq2  11910  fsumconst  12005  ntrivcvgap  12099  prodeq2  12108  p1modz1  12345  bezoutlemmain  12559  dfgcd2  12575  uzwodc  12598  nninfctlemfo  12601  lcmgcdlem  12639  4sqexercise2  12962  4sqlemsdc  12963  mulgval  13699  cnpnei  14933  cnntr  14939  txmetcnp  15232  mpomulcn  15280  lgsval  15723  upgriswlkdc  16157  pw1nct  16540  peano4nninf  16544