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  6736  phpm  7120  phplem4on  7122  fidifsnen  7125  fisbth  7140  fin0  7142  fin0or  7143  fiintim  7191  fisseneq  7195  djudom  7384  difinfsnlem  7390  nnnninfeq  7419  nnnninfeq2  7420  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  exmidapne  7574  prmuloc  7881  cauappcvgprlemopl  7961  cauappcvgprlemdisj  7966  cauappcvgprlemladdfl  7970  caucvgprlemopl  7984  axcaucvglemcau  8213  xnn0letri  10136  xaddf  10177  xleaddadd  10220  ssfzo12bi  10570  rebtwn2zlemstep  10612  btwnzge0  10660  addmodlteq  10760  frecuzrdgg  10778  qsqeqor  11012  apexp1  11080  hashxp  11191  ccatcl  11281  swrdccat3blem  11431  cjap  11591  caucvgre  11666  minmax  11915  xrminmax  11950  sumeq2  12044  fsumconst  12140  ntrivcvgap  12234  prodeq2  12243  p1modz1  12480  bezoutlemmain  12694  dfgcd2  12710  uzwodc  12733  nninfctlemfo  12736  lcmgcdlem  12774  4sqexercise2  13097  4sqlemsdc  13098  mulgval  13839  cnpnei  15084  cnntr  15090  txmetcnp  15383  mpomulcn  15431  lgsval  15877  upgriswlkdc  16355  pw1nct  16777  peano4nninf  16784