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  10215  xaddf  10256  xleaddadd  10299  ssfzo12bi  10653  rebtwn2zlemstep  10697  btwnzge0  10748  addmodlteq  10848  frecuzrdgg  10866  qsqeqor  11100  apexp1  11170  hashxp  11281  ccatcl  11375  swrdccat3blem  11525  cjap  11686  caucvgre  11761  minmax  12011  xrminmax  12047  sumeq2  12141  fsumconst  12237  ntrivcvgap  12331  prodeq2  12340  p1modz1  12577  bezoutlemmain  12791  dfgcd2  12807  uzwodc  12830  nninfctlemfo  12833  lcmgcdlem  12871  pwbdvdseu  12963  sqrtrirr  13005  4sqexercise2  13198  4sqlemsdc  13199  mulgval  13974  gsumconstcmn  14215  cnpnei  15369  cnntr  15375  txmetcnp  15668  mpomulcn  15716  lgsval  16221  upgriswlkdc  16699  pw1nct  17131  peano4nninf  17147