Theorem adantrr 476

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 108	. 2 |- ( ( ps /\ th ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 284	1 |- ( ( ph /\ ( ps /\ th ) ) -> ch )

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:  ad2ant2r  506  ad2ant2lr  507  dn1dc  955  3ad2antr1  1157  xordidc  1394  po2nr  4292  sotricim  4306  fmptco  5659  fvtp1g  5701  dff13  5744  fcof1o  5765  isocnv  5787  isores2  5789  isoini  5794  f1oiso2  5803  acexmidlemab  5844  ovmpodf  5981  offval  6065  xp1st  6141  1stconst  6197  cnvf1olem  6200  f1od2  6211  mpoxopoveq  6216  nnaordi  6484  nnmordi  6492  erinxp  6583  dom2lem  6746  fundmen  6780  mapen  6820  ssenen  6825  fidifsnen  6844  difinfsnlem  7072  fodjum  7118  cc2lem  7215  ltsonq  7347  lt2addnq  7353  lt2mulnq  7354  ltexnqq  7357  prarloclemarch2  7368  enq0sym  7381  genprndl  7470  genprndu  7471  prmuloc  7515  distrlem1prl  7531  distrlem1pru  7532  ltsopr  7545  ltexprlemdisj  7555  ltexprlemfl  7558  ltexprlemfu  7560  addcanprlemu  7564  ltaprg  7568  mulcmpblnrlemg  7689  recexgt0sr  7722  mul4  8038  2addsub  8120  muladd  8290  ltleadd  8352  eqord1  8389  eqord2  8390  divmulap3  8581  divcanap7  8625  divadddivap  8631  lemul2a  8762  lemul12b  8764  ltmuldiv2  8778  ltdivmul  8779  ltdivmul2  8781  ledivmul2  8783  lemuldiv2  8785  lt2msq  8789  cju  8864  zextlt  9291  xrlttr  9739  xrre3  9766  ixxdisj  9847  iooshf  9896  icodisj  9936  iccf1o  9948  expsubap  10511  bcval5  10684  hashfacen  10758  seq3coll  10764  sqrt0rlem  10954  lenegsq  11046  zsumdc  11334  fisum0diag2  11397  prodmodclem2  11527  zproddc  11529  ndvdsadd  11877  zssinfcl  11890  lcmdvds  12020  oddpwdclemdc  12114  hashdvds  12162  phisum  12181  pcqmul  12244  pcmpt  12282  ennnfonelemex  12356  eltg2  12768  ssnei2  12872  restopnb  12896  txdis1cn  12993  txlm  12994  elbl2ps  13107  elbl2  13108  blininf  13139  xmeter  13151  xmetresbl  13155  bdxmet  13216  metrest  13221  dedekindicc  13326  limcimo  13349