Theorem adantrr 462

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantrr	|- ( ( ph /\ ( ps /\ th ) ) -> ch )

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 107	. 2 |- ( ( ps /\ th ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 280	1 |- ( ( ph /\ ( ps /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  ad2ant2r  492  ad2ant2lr  493  dn1dc  901  3ad2antr1  1103  xordidc  1330  po2nr  4064  sotricim  4078  fmptco  5351  fvtp1g  5390  dff13  5428  fcof1o  5449  isocnv  5471  isores2  5473  isoini  5477  f1oiso2  5486  acexmidlemab  5526  ovmpt2df  5652  offval  5739  xp1st  5812  1stconst  5862  cnvf1olem  5865  f1od2  5876  mpt2xopoveq  5878  nnaordi  6104  nnmordi  6112  erinxp  6203  dom2lem  6275  fundmen  6309  fidifsnen  6355  ltsonq  6588  lt2addnq  6594  lt2mulnq  6595  ltexnqq  6598  prarloclemarch2  6609  enq0sym  6622  genprndl  6711  genprndu  6712  prmuloc  6756  distrlem1prl  6772  distrlem1pru  6773  ltsopr  6786  ltexprlemdisj  6796  ltexprlemfl  6799  ltexprlemfu  6801  addcanprlemu  6805  ltaprg  6809  mulcmpblnrlemg  6917  recexgt0sr  6950  mul4  7240  2addsub  7322  muladd  7488  ltleadd  7550  divmulap3  7765  divcanap7  7809  divadddivap  7815  lemul2a  7937  lemul12b  7939  ltmuldiv2  7953  ltdivmul  7954  ltdivmul2  7956  ledivmul2  7958  lemuldiv2  7960  lt2msq  7964  cju  8038  zextlt  8439  xrlttr  8870  xrre3  8889  ixxdisj  8926  iooshf  8975  icodisj  9014  iccf1o  9026  expsubap  9524  ibcval5  9690  sqrt0rlem  9889  lenegsq  9981  ndvdsadd  10331  zssinfcl  10344  lcmdvds  10461  oddpwdclemdc  10551