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  6515  nnaordi  6785  nnmordi  6793  erinxp  6887  dom2lem  7062  fundmen  7098  pw2f1odclem  7138  mapen  7150  ssenen  7156  fidifsnen  7176  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  9749  xrlttr  10214  xrre3  10241  ixxdisj  10322  iooshf  10371  icodisj  10411  iccf1o  10424  zssinfcl  10682  seqf1og  10979  expsubap  11045  bcval5  11223  hashmap  11290  hashfacen  11306  seq3coll  11316  swrdswrdlem  11498  swrdccatin2  11523  sqrt0rlem  11791  lenegsq  11884  zsumdc  12176  fisum0diag2  12239  prodmodclem2  12369  zproddc  12371  ndvdsadd  12723  lcmdvds  12882  hashdvds  13028  phisum  13048  pcqmul  13111  pcmpt  13151  4sqlemffi  13204  4sqlem11  13209  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemex  13363  grpinvid1  13916  grpinvid2  13917  grplcan  13926  grpnpncan0  13960  dfgrp3mlem  13962  dfgrp3m  13963  grplactcnv  13966  0nsg  14076  eqger  14086  resghm  14122  conjghm  14138  znunit  15103  issubassa3  15121  issubassa2  15144  psrbagconf1o  15174  psrgrp  15195  eltg2  15279  ssnei2  15383  restopnb  15407  txdis1cn  15504  txlm  15505  elbl2ps  15618  elbl2  15619  blininf  15650  xmeter  15662  xmetresbl  15666  bdxmet  15727  metrest  15732  dedekindicc  15859  limcimo  15891  dvmptfsum  15951  plycolemc  15984  logdivlt  16124  dvdsppwf1o  16283  fsumdvdsmul  16285  sgmmul  16290  bposlem1  16311  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  upgriswlkdc  16806