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  6781  phpm  7173  phplem4on  7175  fidifsnen  7178  fisbth  7193  fin0  7195  fin0or  7196  fiintim  7244  fisseneq  7248  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  10221  xaddf  10262  xleaddadd  10305  ssfzo12bi  10659  rebtwn2zlemstep  10703  btwnzge0  10755  addmodlteq  10855  frecuzrdgg  10873  qsqeqor  11107  apexp1  11177  hashxp  11288  ccatcl  11382  swrdccat3blem  11532  cjap  11693  caucvgre  11768  minmax  12019  xrminmax  12055  sumeq2  12149  fsumconst  12245  ntrivcvgap  12339  prodeq2  12348  p1modz1  12585  bezoutlemmain  12799  dfgcd2  12815  uzwodc  12838  nninfctlemfo  12841  lcmgcdlem  12879  pwbdvdseu  12971  sqrtrirr  13013  4sqexercise2  13206  4sqlemsdc  13207  mulgval  13983  gsumconstcmn  14265  psrass1fi  15210  cnpnei  15462  cnntr  15468  txmetcnp  15761  mpomulcn  15809  lgsval  16345  upgriswlkdc  16823  pw1nct  17255  peano4nninf  17272