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  8458  2addsub  8540  muladd  8711  ltleadd  8774  eqord1  8811  eqord2  8812  divmulap3  9007  divcanap7  9051  divadddivap  9057  lemul2a  9189  lemul12b  9191  ltmuldiv2  9205  ltdivmul  9206  ltdivmul2  9208  ledivmul2  9210  lemuldiv2  9212  lt2msq  9216  cju  9291  zextlt  9738  xrlttr  10197  xrre3  10224  ixxdisj  10305  iooshf  10354  icodisj  10394  iccf1o  10407  zssinfcl  10665  seqf1og  10958  expsubap  11024  bcval5  11201  hashmap  11268  hashfacen  11284  seq3coll  11294  swrdswrdlem  11476  swrdccatin2  11501  sqrt0rlem  11769  lenegsq  11861  zsumdc  12151  fisum0diag2  12214  prodmodclem2  12344  zproddc  12346  ndvdsadd  12698  lcmdvds  12857  oddpwdclemdc  12951  hashdvds  12999  phisum  13019  pcqmul  13082  pcmpt  13122  4sqlemffi  13175  4sqlem11  13180  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemex  13305  grpinvid1  13857  grpinvid2  13858  grplcan  13867  grpnpncan0  13901  dfgrp3mlem  13903  dfgrp3m  13904  grplactcnv  13907  0nsg  14017  eqger  14027  resghm  14063  conjghm  14079  znunit  14994  issubassa3  15012  issubassa2  15035  psrbagconf1o  15064  psrgrp  15076  eltg2  15154  ssnei2  15258  restopnb  15282  txdis1cn  15379  txlm  15380  elbl2ps  15493  elbl2  15494  blininf  15525  xmeter  15537  xmetresbl  15541  bdxmet  15602  metrest  15607  dedekindicc  15734  limcimo  15766  dvmptfsum  15826  plycolemc  15859  dvdsppwf1o  16103  fsumdvdsmul  16105  sgmmul  16110  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  upgriswlkdc  16601