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 )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad2ant2r  513  ad2ant2lr  514  dn1dc  973  3ad2antr1  1193  xordidc  1448  po2nr  4449  sotricim  4463  fmptco  5865  fvtp1g  5914  dff13  5964  fcof1o  5985  isocnv  6007  isores2  6009  isoini  6014  f1oiso2  6023  acexmidlemab  6069  ovmpodf  6210  offval  6300  xp1st  6389  1stconst  6447  cnvf1olem  6450  f1od2  6461  mpoxopoveq  6501  nnaordi  6771  nnmordi  6779  erinxp  6873  dom2lem  7048  fundmen  7084  pw2f1odclem  7124  mapen  7136  ssenen  7142  fidifsnen  7162  difinfsnlem  7429  fodjum  7476  cc2lem  7622  ltsonq  7755  lt2addnq  7761  lt2mulnq  7762  ltexnqq  7765  prarloclemarch2  7776  enq0sym  7789  genprndl  7878  genprndu  7879  prmuloc  7923  distrlem1prl  7939  distrlem1pru  7940  ltsopr  7953  ltexprlemdisj  7963  ltexprlemfl  7966  ltexprlemfu  7968  addcanprlemu  7972  ltaprg  7976  mulcmpblnrlemg  8097  recexgt0sr  8130  mul4  8448  2addsub  8530  muladd  8701  ltleadd  8764  eqord1  8801  eqord2  8802  divmulap3  8997  divcanap7  9041  divadddivap  9047  lemul2a  9179  lemul12b  9181  ltmuldiv2  9195  ltdivmul  9196  ltdivmul2  9198  ledivmul2  9200  lemuldiv2  9202  lt2msq  9206  cju  9281  zextlt  9717  xrlttr  10176  xrre3  10203  ixxdisj  10284  iooshf  10333  icodisj  10373  iccf1o  10386  zssinfcl  10643  seqf1og  10936  expsubap  11002  bcval5  11179  hashmap  11246  hashfacen  11262  seq3coll  11272  swrdswrdlem  11454  swrdccatin2  11479  sqrt0rlem  11747  lenegsq  11839  zsumdc  12129  fisum0diag2  12192  prodmodclem2  12322  zproddc  12324  ndvdsadd  12676  lcmdvds  12835  oddpwdclemdc  12929  hashdvds  12977  phisum  12997  pcqmul  13060  pcmpt  13100  4sqlemffi  13153  4sqlem11  13158  ballotfilemfc0  13210  ballotfilemfcc  13211  ennnfonelemex  13283  grpinvid1  13834  grpinvid2  13835  grplcan  13844  grpnpncan0  13878  dfgrp3mlem  13880  dfgrp3m  13881  grplactcnv  13884  0nsg  13994  eqger  14004  resghm  14040  conjghm  14056  znunit  14966  psrbagconf1o  14987  psrgrp  14999  eltg2  15077  ssnei2  15181  restopnb  15205  txdis1cn  15302  txlm  15303  elbl2ps  15416  elbl2  15417  blininf  15448  xmeter  15460  xmetresbl  15464  bdxmet  15525  metrest  15530  dedekindicc  15657  limcimo  15689  dvmptfsum  15749  plycolemc  15782  dvdsppwf1o  16017  fsumdvdsmul  16019  sgmmul  16024  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  upgriswlkdc  16515