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  po2nr  4454  sotricim  4468  fmptco  5874  fvtp1g  5923  dff13  5974  fcof1o  5995  isocnv  6017  isores2  6019  isoini  6024  f1oiso2  6033  acexmidlemab  6079  ovmpodf  6220  offval  6310  xp1st  6399  1stconst  6457  cnvf1olem  6460  f1od2  6471  mpoxopoveq  6511  nnaordi  6781  nnmordi  6789  erinxp  6883  dom2lem  7058  fundmen  7094  pw2f1odclem  7134  mapen  7146  ssenen  7152  fidifsnen  7172  difinfsnlem  7439  fodjum  7486  cc2lem  7632  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  ltexnqq  7775  prarloclemarch2  7786  enq0sym  7799  genprndl  7888  genprndu  7889  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  ltexprlemdisj  7973  ltexprlemfl  7976  ltexprlemfu  7978  addcanprlemu  7982  ltaprg  7986  mulcmpblnrlemg  8107  recexgt0sr  8140  mul4  8459  2addsub  8541  muladd  8712  ltleadd  8775  eqord1  8812  eqord2  8813  divmulap3  9009  divcanap7  9053  divadddivap  9059  lemul2a  9191  lemul12b  9193  ltmuldiv2  9207  ltdivmul  9208  ltdivmul2  9210  ledivmul2  9212  lemuldiv2  9214  lt2msq  9218  cju  9293  zextlt  9742  xrlttr  10207  xrre3  10234  ixxdisj  10315  iooshf  10364  icodisj  10404  iccf1o  10417  zssinfcl  10675  seqf1og  10971  expsubap  11037  bcval5  11215  hashmap  11282  hashfacen  11298  seq3coll  11308  swrdswrdlem  11490  swrdccatin2  11515  sqrt0rlem  11783  lenegsq  11876  zsumdc  12167  fisum0diag2  12230  prodmodclem2  12360  zproddc  12362  ndvdsadd  12714  lcmdvds  12873  hashdvds  13019  phisum  13039  pcqmul  13102  pcmpt  13142  4sqlemffi  13195  4sqlem11  13200  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemex  13354  grpinvid1  13906  grpinvid2  13907  grplcan  13916  grpnpncan0  13950  dfgrp3mlem  13952  dfgrp3m  13953  grplactcnv  13956  0nsg  14066  eqger  14076  resghm  14112  conjghm  14128  znunit  15043  issubassa3  15061  issubassa2  15084  psrbagconf1o  15113  psrgrp  15125  eltg2  15203  ssnei2  15307  restopnb  15331  txdis1cn  15428  txlm  15429  elbl2ps  15542  elbl2  15543  blininf  15574  xmeter  15586  xmetresbl  15590  bdxmet  15651  metrest  15656  dedekindicc  15783  limcimo  15815  dvmptfsum  15875  plycolemc  15908  logdivlt  16046  dvdsppwf1o  16184  fsumdvdsmul  16186  sgmmul  16191  bposlem1  16209  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  upgriswlkdc  16699