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  6749  phpm  7133  phplem4on  7135  fidifsnen  7138  fisbth  7153  fin0  7155  fin0or  7156  fiintim  7204  fisseneq  7208  djudom  7397  difinfsnlem  7403  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  exmidapne  7590  prmuloc  7897  cauappcvgprlemopl  7977  cauappcvgprlemdisj  7982  cauappcvgprlemladdfl  7986  caucvgprlemopl  8000  axcaucvglemcau  8229  xnn0letri  10155  xaddf  10196  xleaddadd  10239  ssfzo12bi  10592  rebtwn2zlemstep  10636  btwnzge0  10684  addmodlteq  10784  frecuzrdgg  10802  qsqeqor  11036  apexp1  11105  hashxp  11216  ccatcl  11306  swrdccat3blem  11456  cjap  11616  caucvgre  11691  minmax  11940  xrminmax  11975  sumeq2  12069  fsumconst  12165  ntrivcvgap  12259  prodeq2  12268  p1modz1  12505  bezoutlemmain  12719  dfgcd2  12735  uzwodc  12758  nninfctlemfo  12761  lcmgcdlem  12799  4sqexercise2  13122  4sqlemsdc  13123  mulgval  13875  cnpnei  15210  cnntr  15216  txmetcnp  15509  mpomulcn  15557  lgsval  16003  upgriswlkdc  16481  pw1nct  16903  peano4nninf  16910