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 )

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  499  nntr2  6766  phpm  7157  phplem4on  7159  fidifsnen  7162  fisbth  7177  fin0  7179  fin0or  7180  fiintim  7228  fisseneq  7232  djudom  7423  difinfsnlem  7429  nnnninfeq  7458  nnnninfeq2  7459  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  exmidapne  7616  prmuloc  7923  cauappcvgprlemopl  8003  cauappcvgprlemdisj  8008  cauappcvgprlemladdfl  8012  caucvgprlemopl  8026  axcaucvglemcau  8255  xnn0letri  10184  xaddf  10225  xleaddadd  10268  ssfzo12bi  10621  rebtwn2zlemstep  10665  btwnzge0  10713  addmodlteq  10813  frecuzrdgg  10831  qsqeqor  11065  apexp1  11134  hashxp  11245  ccatcl  11339  swrdccat3blem  11489  cjap  11650  caucvgre  11725  minmax  11974  xrminmax  12009  sumeq2  12103  fsumconst  12199  ntrivcvgap  12293  prodeq2  12302  p1modz1  12539  bezoutlemmain  12753  dfgcd2  12769  uzwodc  12792  nninfctlemfo  12795  lcmgcdlem  12833  4sqexercise2  13156  4sqlemsdc  13157  mulgval  13902  gsumconstcmn  14143  cnpnei  15243  cnntr  15249  txmetcnp  15542  mpomulcn  15590  lgsval  16037  upgriswlkdc  16515  pw1nct  16947  peano4nninf  16954