Theorem adantrl 482

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
adantrl	|- ( ( ph /\ ( th /\ ps ) ) -> ch )

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( th /\ ps ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 286	1 |- ( ( ph /\ ( th /\ ps ) ) -> 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:  ad2ant2l  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4813  foco  5629  fvun1  5772  isocnv  6020  isores2  6022  f1oiso2  6036  offval  6314  xp2nd  6404  1stconst  6461  2ndconst  6462  tfrlem9  6595  nnmordi  6794  dom2lem  7064  fundmen  7100  mapen  7152  mapunen  7157  ssenen  7158  ltsonq  7771  ltexnqq  7781  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemfl  7982  ltexprlemfu  7984  mulcmpblnrlemg  8113  cnegexlem2  8509  muladd  8718  eqord1  8818  eqord2  8819  divadddivap  9065  ltmul12a  9198  lemul12b  9199  cju  9299  zextlt  9748  supinfneg  10010  infsupneg  10011  xrre  10238  ixxdisj  10321  iooshf  10370  icodisj  10410  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  iccf1o  10423  fzaddel  10481  fzsubel  10482  seq3caopr  10952  seqcaoprg  10953  expineg2  11005  expsubap  11044  expnbnd  11121  facndiv  11198  hashfibclem  11303  hashfacen  11305  hashf1lem1  11306  ccatpfx  11494  swrdccatfn  11517  swrdccatin2  11522  fprodeq0  12408  lcmdvds  12881  hashdvds  13027  eulerthlemh  13037  pceu  13102  pcqcl  13113  infpnlem1  13166  4sqlem11  13208  mhmpropd  13831  subsubm  13848  grplcan  13925  grplmulf1o  13937  dfgrp3mlem  13961  mulgfng  13985  mulgsubcl  13997  subsubg  14058  eqger  14085  resghm  14121  conjghm  14137  subsubrng  14630  subsubrg  14661  issubassa2  15143  psrbagconf1o  15177  psrgrp  15204  txlm  15522  blininf  15667  xmeter  15679  xmetresbl  15683  limcimo  15908  dvdsppwf1o  16300  fsumdvdsmul  16302  sgmmul  16307  bposlem6  16333  clwwlkn1loopb  16883