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  6657  phpm  7035  phplem4on  7037  fidifsnen  7040  fisbth  7053  fin0  7055  fin0or  7056  fiintim  7104  fisseneq  7107  djudom  7271  difinfsnlem  7277  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  exmidapne  7457  prmuloc  7764  cauappcvgprlemopl  7844  cauappcvgprlemdisj  7849  cauappcvgprlemladdfl  7853  caucvgprlemopl  7867  axcaucvglemcau  8096  xnn0letri  10011  xaddf  10052  xleaddadd  10095  ssfzo12bi  10443  rebtwn2zlemstep  10484  btwnzge0  10532  addmodlteq  10632  frecuzrdgg  10650  qsqeqor  10884  apexp1  10952  hashxp  11061  ccatcl  11141  swrdccat3blem  11286  cjap  11432  caucvgre  11507  minmax  11756  xrminmax  11791  sumeq2  11885  fsumconst  11980  ntrivcvgap  12074  prodeq2  12083  p1modz1  12320  bezoutlemmain  12534  dfgcd2  12550  uzwodc  12573  nninfctlemfo  12576  lcmgcdlem  12614  4sqexercise2  12937  4sqlemsdc  12938  mulgval  13674  cnpnei  14908  cnntr  14914  txmetcnp  15207  mpomulcn  15255  lgsval  15698  upgriswlkdc  16101  pw1nct  16428  peano4nninf  16432