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  6780  phpm  7171  phplem4on  7173  fidifsnen  7176  fisbth  7191  fin0  7193  fin0or  7194  fiintim  7242  fisseneq  7246  djudom  7439  difinfsnlem  7445  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  exmidapne  7632  prmuloc  7939  cauappcvgprlemopl  8019  cauappcvgprlemdisj  8024  cauappcvgprlemladdfl  8028  caucvgprlemopl  8042  axcaucvglemcau  8271  xnn0letri  10222  xaddf  10263  xleaddadd  10306  ssfzo12bi  10660  rebtwn2zlemstep  10704  btwnzge0  10756  addmodlteq  10856  frecuzrdgg  10874  qsqeqor  11108  apexp1  11178  hashxp  11289  ccatcl  11383  swrdccat3blem  11533  cjap  11694  caucvgre  11769  minmax  12020  xrminmax  12056  sumeq2  12150  fsumconst  12246  ntrivcvgap  12340  prodeq2  12349  p1modz1  12586  bezoutlemmain  12800  dfgcd2  12816  uzwodc  12839  nninfctlemfo  12842  lcmgcdlem  12880  pwbdvdseu  12972  sqrtrirr  13014  4sqexercise2  13207  4sqlemsdc  13208  mulgval  13984  gsumconstcmn  14266  psrass1fi  15201  cnpnei  15445  cnntr  15451  txmetcnp  15744  mpomulcn  15792  lgsval  16328  upgriswlkdc  16806  pw1nct  17238  peano4nninf  17255