Theorem adantrr 483

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

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:  ad2ant2r  513  ad2ant2lr  514  dn1dc  973  3ad2antr1  1193  xordidc  1448  sn0disj  4127  po2nr  4456  sotricim  4470  fmptco  5877  fvtp1g  5926  dff13  5977  fcof1o  5998  isocnv  6020  isores2  6022  isoini  6027  f1oiso2  6036  acexmidlemab  6082  ovmpodf  6223  offval  6314  xp1st  6403  1stconst  6461  cnvf1olem  6464  f1od2  6475  mpoxopoveq  6516  nnaordi  6786  nnmordi  6794  erinxp  6888  dom2lem  7064  fundmen  7100  pw2f1odclem  7140  mapen  7152  ssenen  7158  fidifsnen  7178  difinfsnlem  7445  fodjum  7492  cc2lem  7638  ltsonq  7771  lt2addnq  7777  lt2mulnq  7778  ltexnqq  7781  prarloclemarch2  7792  enq0sym  7805  genprndl  7894  genprndu  7895  prmuloc  7939  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  ltexprlemdisj  7979  ltexprlemfl  7982  ltexprlemfu  7984  addcanprlemu  7988  ltaprg  7992  mulcmpblnrlemg  8113  recexgt0sr  8146  mul4  8465  2addsub  8547  muladd  8718  ltleadd  8781  eqord1  8818  eqord2  8819  divmulap3  9015  divcanap7  9059  divadddivap  9065  lemul2a  9197  lemul12b  9199  ltmuldiv2  9213  ltdivmul  9214  ltdivmul2  9216  ledivmul2  9218  lemuldiv2  9220  lt2msq  9224  cju  9299  zextlt  9748  xrlttr  10213  xrre3  10240  ixxdisj  10321  iooshf  10370  icodisj  10410  iccf1o  10423  zssinfcl  10681  seqf1og  10978  expsubap  11044  bcval5  11222  hashmap  11289  hashfacen  11305  seq3coll  11315  swrdswrdlem  11497  swrdccatin2  11522  sqrt0rlem  11790  lenegsq  11883  zsumdc  12175  fisum0diag2  12238  prodmodclem2  12368  zproddc  12370  ndvdsadd  12722  lcmdvds  12881  hashdvds  13027  phisum  13047  pcqmul  13110  pcmpt  13150  4sqlemffi  13203  4sqlem11  13208  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemex  13362  grpinvid1  13915  grpinvid2  13916  grplcan  13925  grpnpncan0  13959  dfgrp3mlem  13961  dfgrp3m  13962  grplactcnv  13965  0nsg  14075  eqger  14085  resghm  14121  conjghm  14137  znunit  15102  issubassa3  15120  issubassa2  15143  psrbagconf1o  15177  psrgrp  15204  eltg2  15296  ssnei2  15400  restopnb  15424  txdis1cn  15521  txlm  15522  elbl2ps  15635  elbl2  15636  blininf  15667  xmeter  15679  xmetresbl  15683  bdxmet  15744  metrest  15749  dedekindicc  15876  limcimo  15908  dvmptfsum  15968  plycolemc  16001  logdivlt  16141  dvdsppwf1o  16300  fsumdvdsmul  16302  sgmmul  16307  bposlem1  16328  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  upgriswlkdc  16823