Theorem ad3antlr 497

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 493	. 2 |- ( ( ( ch /\ ph ) /\ th ) -> ps )
3	2	adantr 276	1 |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antlr  499  nntr2  6776  phpm  7167  phplem4on  7169  fidifsnen  7172  fisbth  7187  fin0  7189  fin0or  7190  fiintim  7238  fisseneq  7242  djudom  7433  difinfsnlem  7439  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  exmidapne  7626  prmuloc  7933  cauappcvgprlemopl  8013  cauappcvgprlemdisj  8018  cauappcvgprlemladdfl  8022  caucvgprlemopl  8036  axcaucvglemcau  8265  xnn0letri  10205  xaddf  10246  xleaddadd  10289  ssfzo12bi  10643  rebtwn2zlemstep  10687  btwnzge0  10735  addmodlteq  10835  frecuzrdgg  10853  qsqeqor  11087  apexp1  11156  hashxp  11267  ccatcl  11361  swrdccat3blem  11511  cjap  11672  caucvgre  11747  minmax  11996  xrminmax  12031  sumeq2  12125  fsumconst  12221  ntrivcvgap  12315  prodeq2  12324  p1modz1  12561  bezoutlemmain  12775  dfgcd2  12791  uzwodc  12814  nninfctlemfo  12817  lcmgcdlem  12855  4sqexercise2  13178  4sqlemsdc  13179  mulgval  13925  gsumconstcmn  14166  cnpnei  15320  cnntr  15326  txmetcnp  15619  mpomulcn  15667  lgsval  16123  upgriswlkdc  16601  pw1nct  17033  peano4nninf  17049