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  6443  phpm  6803  phplem4on  6805  fidifsnen  6808  fisbth  6821  fin0  6823  fin0or  6824  fiintim  6866  fisseneq  6869  djudom  7027  difinfsnlem  7033  enomnilem  7064  enmkvlem  7087  enwomnilem  7095  prmuloc  7469  cauappcvgprlemopl  7549  cauappcvgprlemdisj  7554  cauappcvgprlemladdfl  7558  caucvgprlemopl  7572  axcaucvglemcau  7801  xaddf  9730  xleaddadd  9773  ssfzo12bi  10106  rebtwn2zlemstep  10134  btwnzge0  10181  addmodlteq  10279  frecuzrdgg  10297  apexp1  10574  hashxp  10682  cjap  10788  caucvgre  10863  minmax  11111  xrminmax  11144  sumeq2  11238  fsumconst  11333  ntrivcvgap  11427  prodeq2  11436  p1modz1  11672  bezoutlemmain  11862  dfgcd2  11878  lcmgcdlem  11934  cnpnei  12579  cnntr  12585  txmetcnp  12878  pw1nct  13535  peano4nninf  13539  nninfalllemn  13541