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  968  3ad2antr1  1188  xordidc  1443  po2nr  4406  sotricim  4420  fmptco  5813  fvtp1g  5862  dff13  5909  fcof1o  5930  isocnv  5952  isores2  5954  isoini  5959  f1oiso2  5968  acexmidlemab  6012  ovmpodf  6153  offval  6243  xp1st  6328  1stconst  6386  cnvf1olem  6389  f1od2  6400  mpoxopoveq  6406  nnaordi  6676  nnmordi  6684  erinxp  6778  dom2lem  6945  fundmen  6981  pw2f1odclem  7020  mapen  7032  ssenen  7037  fidifsnen  7057  difinfsnlem  7298  fodjum  7345  cc2lem  7485  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  ltexnqq  7628  prarloclemarch2  7639  enq0sym  7652  genprndl  7741  genprndu  7742  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  addcanprlemu  7835  ltaprg  7839  mulcmpblnrlemg  7960  recexgt0sr  7993  mul4  8311  2addsub  8393  muladd  8563  ltleadd  8626  eqord1  8663  eqord2  8664  divmulap3  8857  divcanap7  8901  divadddivap  8907  lemul2a  9039  lemul12b  9041  ltmuldiv2  9055  ltdivmul  9056  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  lt2msq  9066  cju  9141  zextlt  9572  xrlttr  10030  xrre3  10057  ixxdisj  10138  iooshf  10187  icodisj  10227  iccf1o  10239  zssinfcl  10493  seqf1og  10784  expsubap  10850  bcval5  11026  hashfacen  11101  seq3coll  11107  swrdswrdlem  11289  swrdccatin2  11314  sqrt0rlem  11581  lenegsq  11673  zsumdc  11963  fisum0diag2  12026  prodmodclem2  12156  zproddc  12158  ndvdsadd  12510  lcmdvds  12669  oddpwdclemdc  12763  hashdvds  12811  phisum  12831  pcqmul  12894  pcmpt  12934  4sqlemffi  12987  4sqlem11  12992  ennnfonelemex  13053  grpinvid1  13653  grpinvid2  13654  grplcan  13663  grpnpncan0  13697  dfgrp3mlem  13699  dfgrp3m  13700  grplactcnv  13703  0nsg  13819  eqger  13829  resghm  13865  conjghm  13881  znunit  14692  psrgrp  14718  eltg2  14796  ssnei2  14900  restopnb  14924  txdis1cn  15021  txlm  15022  elbl2ps  15135  elbl2  15136  blininf  15167  xmeter  15179  xmetresbl  15183  bdxmet  15244  metrest  15249  dedekindicc  15376  limcimo  15408  dvmptfsum  15468  plycolemc  15501  dvdsppwf1o  15732  fsumdvdsmul  15734  sgmmul  15739  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  upgriswlkdc  16230