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  963  3ad2antr1  1165  xordidc  1419  po2nr  4364  sotricim  4378  fmptco  5759  fvtp1g  5805  dff13  5850  fcof1o  5871  isocnv  5893  isores2  5895  isoini  5900  f1oiso2  5909  acexmidlemab  5951  ovmpodf  6090  offval  6179  xp1st  6264  1stconst  6320  cnvf1olem  6323  f1od2  6334  mpoxopoveq  6339  nnaordi  6607  nnmordi  6615  erinxp  6709  dom2lem  6876  fundmen  6912  pw2f1odclem  6946  mapen  6958  ssenen  6963  fidifsnen  6982  difinfsnlem  7216  fodjum  7263  cc2lem  7398  ltsonq  7531  lt2addnq  7537  lt2mulnq  7538  ltexnqq  7541  prarloclemarch2  7552  enq0sym  7565  genprndl  7654  genprndu  7655  prmuloc  7699  distrlem1prl  7715  distrlem1pru  7716  ltsopr  7729  ltexprlemdisj  7739  ltexprlemfl  7742  ltexprlemfu  7744  addcanprlemu  7748  ltaprg  7752  mulcmpblnrlemg  7873  recexgt0sr  7906  mul4  8224  2addsub  8306  muladd  8476  ltleadd  8539  eqord1  8576  eqord2  8577  divmulap3  8770  divcanap7  8814  divadddivap  8820  lemul2a  8952  lemul12b  8954  ltmuldiv2  8968  ltdivmul  8969  ltdivmul2  8971  ledivmul2  8973  lemuldiv2  8975  lt2msq  8979  cju  9054  zextlt  9485  xrlttr  9937  xrre3  9964  ixxdisj  10045  iooshf  10094  icodisj  10134  iccf1o  10146  zssinfcl  10397  seqf1og  10688  expsubap  10754  bcval5  10930  hashfacen  11003  seq3coll  11009  swrdswrdlem  11180  sqrt0rlem  11389  lenegsq  11481  zsumdc  11770  fisum0diag2  11833  prodmodclem2  11963  zproddc  11965  ndvdsadd  12317  lcmdvds  12476  oddpwdclemdc  12570  hashdvds  12618  phisum  12638  pcqmul  12701  pcmpt  12741  4sqlemffi  12794  4sqlem11  12799  ennnfonelemex  12860  grpinvid1  13459  grpinvid2  13460  grplcan  13469  grpnpncan0  13503  dfgrp3mlem  13505  dfgrp3m  13506  grplactcnv  13509  0nsg  13625  eqger  13635  resghm  13671  conjghm  13687  znunit  14496  psrgrp  14522  eltg2  14600  ssnei2  14704  restopnb  14728  txdis1cn  14825  txlm  14826  elbl2ps  14939  elbl2  14940  blininf  14971  xmeter  14983  xmetresbl  14987  bdxmet  15048  metrest  15053  dedekindicc  15180  limcimo  15212  dvmptfsum  15272  plycolemc  15305  dvdsppwf1o  15536  fsumdvdsmul  15538  sgmmul  15543  lgsquadlem1  15629  lgsquadlem2  15630  lgsquad2lem2  15634