Theorem adantrr 479

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  509  ad2ant2lr  510  dn1dc  962  3ad2antr1  1164  xordidc  1410  po2nr  4341  sotricim  4355  fmptco  5725  fvtp1g  5767  dff13  5812  fcof1o  5833  isocnv  5855  isores2  5857  isoini  5862  f1oiso2  5871  acexmidlemab  5913  ovmpodf  6051  offval  6140  xp1st  6220  1stconst  6276  cnvf1olem  6279  f1od2  6290  mpoxopoveq  6295  nnaordi  6563  nnmordi  6571  erinxp  6665  dom2lem  6828  fundmen  6862  pw2f1odclem  6892  mapen  6904  ssenen  6909  fidifsnen  6928  difinfsnlem  7160  fodjum  7207  cc2lem  7328  ltsonq  7460  lt2addnq  7466  lt2mulnq  7467  ltexnqq  7470  prarloclemarch2  7481  enq0sym  7494  genprndl  7583  genprndu  7584  prmuloc  7628  distrlem1prl  7644  distrlem1pru  7645  ltsopr  7658  ltexprlemdisj  7668  ltexprlemfl  7671  ltexprlemfu  7673  addcanprlemu  7677  ltaprg  7681  mulcmpblnrlemg  7802  recexgt0sr  7835  mul4  8153  2addsub  8235  muladd  8405  ltleadd  8467  eqord1  8504  eqord2  8505  divmulap3  8698  divcanap7  8742  divadddivap  8748  lemul2a  8880  lemul12b  8882  ltmuldiv2  8896  ltdivmul  8897  ltdivmul2  8899  ledivmul2  8901  lemuldiv2  8903  lt2msq  8907  cju  8982  zextlt  9412  xrlttr  9864  xrre3  9891  ixxdisj  9972  iooshf  10021  icodisj  10061  iccf1o  10073  seqf1og  10595  expsubap  10661  bcval5  10837  hashfacen  10910  seq3coll  10916  sqrt0rlem  11150  lenegsq  11242  zsumdc  11530  fisum0diag2  11593  prodmodclem2  11723  zproddc  11725  ndvdsadd  12075  zssinfcl  12088  lcmdvds  12220  oddpwdclemdc  12314  hashdvds  12362  phisum  12381  pcqmul  12444  pcmpt  12484  4sqlemffi  12537  4sqlem11  12542  ennnfonelemex  12574  grpinvid1  13127  grpinvid2  13128  grplcan  13137  grpnpncan0  13171  dfgrp3mlem  13173  dfgrp3m  13174  grplactcnv  13177  0nsg  13287  eqger  13297  resghm  13333  conjghm  13349  znunit  14158  eltg2  14232  ssnei2  14336  restopnb  14360  txdis1cn  14457  txlm  14458  elbl2ps  14571  elbl2  14572  blininf  14603  xmeter  14615  xmetresbl  14619  bdxmet  14680  metrest  14685  dedekindicc  14812  limcimo  14844  dvmptfsum  14904  plycolemc  14936  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239