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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antlr  499  nntr2  6776  phpm  7167  phplem4on  7169  fidifsnen  7172  fisbth  7187  fin0  7189  fin0or  7190  fiintim  7238  fisseneq  7242  djudom  7434  difinfsnlem  7440  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  exmidapne  7627  prmuloc  7934  cauappcvgprlemopl  8014  cauappcvgprlemdisj  8019  cauappcvgprlemladdfl  8023  caucvgprlemopl  8037  axcaucvglemcau  8266  xnn0letri  10216  xaddf  10257  xleaddadd  10300  ssfzo12bi  10654  rebtwn2zlemstep  10698  btwnzge0  10750  addmodlteq  10850  frecuzrdgg  10868  qsqeqor  11102  apexp1  11172  hashxp  11283  ccatcl  11377  swrdccat3blem  11527  cjap  11688  caucvgre  11763  minmax  12014  xrminmax  12050  sumeq2  12144  fsumconst  12240  ntrivcvgap  12334  prodeq2  12343  p1modz1  12580  bezoutlemmain  12794  dfgcd2  12810  uzwodc  12833  nninfctlemfo  12836  lcmgcdlem  12874  pwbdvdseu  12966  sqrtrirr  13008  4sqexercise2  13201  4sqlemsdc  13202  mulgval  13978  gsumconstcmn  14250  cnpnei  15411  cnntr  15417  txmetcnp  15710  mpomulcn  15758  lgsval  16289  upgriswlkdc  16767  pw1nct  17199  peano4nninf  17215