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  6503  phpm  6864  phplem4on  6866  fidifsnen  6869  fisbth  6882  fin0  6884  fin0or  6885  fiintim  6927  fisseneq  6930  djudom  7091  difinfsnlem  7097  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  exmidapne  7258  prmuloc  7564  cauappcvgprlemopl  7644  cauappcvgprlemdisj  7649  cauappcvgprlemladdfl  7653  caucvgprlemopl  7667  axcaucvglemcau  7896  xnn0letri  9801  xaddf  9842  xleaddadd  9885  ssfzo12bi  10222  rebtwn2zlemstep  10250  btwnzge0  10297  addmodlteq  10395  frecuzrdgg  10413  qsqeqor  10627  apexp1  10693  hashxp  10801  cjap  10910  caucvgre  10985  minmax  11233  xrminmax  11268  sumeq2  11362  fsumconst  11457  ntrivcvgap  11551  prodeq2  11560  p1modz1  11796  bezoutlemmain  11993  dfgcd2  12009  uzwodc  12032  lcmgcdlem  12071  mulgval  12940  cnpnei  13612  cnntr  13618  txmetcnp  13911  lgsval  14298  pw1nct  14634  peano4nninf  14637