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  7440  fodjum  7487  cc2lem  7633  ltsonq  7766  lt2addnq  7772  lt2mulnq  7773  ltexnqq  7776  prarloclemarch2  7787  enq0sym  7800  genprndl  7889  genprndu  7890  prmuloc  7934  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  ltexprlemdisj  7974  ltexprlemfl  7977  ltexprlemfu  7979  addcanprlemu  7983  ltaprg  7987  mulcmpblnrlemg  8108  recexgt0sr  8141  mul4  8460  2addsub  8542  muladd  8713  ltleadd  8776  eqord1  8813  eqord2  8814  divmulap3  9010  divcanap7  9054  divadddivap  9060  lemul2a  9192  lemul12b  9194  ltmuldiv2  9208  ltdivmul  9209  ltdivmul2  9211  ledivmul2  9213  lemuldiv2  9215  lt2msq  9219  cju  9294  zextlt  9743  xrlttr  10208  xrre3  10235  ixxdisj  10316  iooshf  10365  icodisj  10405  iccf1o  10418  zssinfcl  10676  seqf1og  10973  expsubap  11039  bcval5  11217  hashmap  11284  hashfacen  11300  seq3coll  11310  swrdswrdlem  11492  swrdccatin2  11517  sqrt0rlem  11785  lenegsq  11878  zsumdc  12170  fisum0diag2  12233  prodmodclem2  12363  zproddc  12365  ndvdsadd  12717  lcmdvds  12876  hashdvds  13022  phisum  13042  pcqmul  13105  pcmpt  13145  4sqlemffi  13198  4sqlem11  13203  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemex  13357  grpinvid1  13910  grpinvid2  13911  grplcan  13920  grpnpncan0  13954  dfgrp3mlem  13956  dfgrp3m  13957  grplactcnv  13960  0nsg  14070  eqger  14080  resghm  14116  conjghm  14132  znunit  15078  issubassa3  15096  issubassa2  15119  psrbagconf1o  15149  psrgrp  15167  eltg2  15245  ssnei2  15349  restopnb  15373  txdis1cn  15470  txlm  15471  elbl2ps  15584  elbl2  15585  blininf  15616  xmeter  15628  xmetresbl  15632  bdxmet  15693  metrest  15698  dedekindicc  15825  limcimo  15857  dvmptfsum  15917  plycolemc  15950  logdivlt  16088  dvdsppwf1o  16244  fsumdvdsmul  16246  sgmmul  16251  bposlem1  16272  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  upgriswlkdc  16767