Theorem ad3antlr 485

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4antlr  487  nntr2  6471  phpm  6831  phplem4on  6833  fidifsnen  6836  fisbth  6849  fin0  6851  fin0or  6852  fiintim  6894  fisseneq  6897  djudom  7058  difinfsnlem  7064  nnnninfeq  7092  nnnninfeq2  7093  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  prmuloc  7507  cauappcvgprlemopl  7587  cauappcvgprlemdisj  7592  cauappcvgprlemladdfl  7596  caucvgprlemopl  7610  axcaucvglemcau  7839  xnn0letri  9739  xaddf  9780  xleaddadd  9823  ssfzo12bi  10160  rebtwn2zlemstep  10188  btwnzge0  10235  addmodlteq  10333  frecuzrdgg  10351  qsqeqor  10565  apexp1  10631  hashxp  10739  cjap  10848  caucvgre  10923  minmax  11171  xrminmax  11206  sumeq2  11300  fsumconst  11395  ntrivcvgap  11489  prodeq2  11498  p1modz1  11734  bezoutlemmain  11931  dfgcd2  11947  uzwodc  11970  lcmgcdlem  12009  cnpnei  12859  cnntr  12865  txmetcnp  13158  lgsval  13545  pw1nct  13883  peano4nninf  13886