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  6558  phpm  6923  phplem4on  6925  fidifsnen  6928  fisbth  6941  fin0  6943  fin0or  6944  fiintim  6987  fisseneq  6990  djudom  7154  difinfsnlem  7160  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  exmidapne  7322  prmuloc  7628  cauappcvgprlemopl  7708  cauappcvgprlemdisj  7713  cauappcvgprlemladdfl  7717  caucvgprlemopl  7731  axcaucvglemcau  7960  xnn0letri  9872  xaddf  9913  xleaddadd  9956  ssfzo12bi  10295  rebtwn2zlemstep  10324  btwnzge0  10372  addmodlteq  10472  frecuzrdgg  10490  qsqeqor  10724  apexp1  10792  hashxp  10900  cjap  11053  caucvgre  11128  minmax  11376  xrminmax  11411  sumeq2  11505  fsumconst  11600  ntrivcvgap  11694  prodeq2  11703  p1modz1  11940  bezoutlemmain  12138  dfgcd2  12154  uzwodc  12177  nninfctlemfo  12180  lcmgcdlem  12218  4sqexercise2  12540  4sqlemsdc  12541  mulgval  13195  cnpnei  14398  cnntr  14404  txmetcnp  14697  mpomulcn  14745  lgsval  15161  pw1nct  15563  peano4nninf  15566