Theorem ad2ant2l 782

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad2ant2l	|- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrl 752	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 750	1 |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  funcnvqp  5952  mpteqb  6299  mpt2fun  6762  soxp  7290  wfrlem4  7418  oaass  7641  undifixp  7944  undom  8048  xpdom2  8055  tcrank  8747  inawinalem  9511  addcanpr  9868  ltsosr  9915  1re  10039  add42  10257  muladd  10462  mulsub  10473  divmuleq  10730  ltmul12a  10879  lemul12b  10880  lemul12a  10881  mulge0b  10893  qaddcl  11804  qmulcl  11806  iooshf  12252  fzass4  12379  elfzomelpfzo  12572  modid  12695  cshwleneq  13563  s2eq2seq  13682  tanaddlem  14896  fpwipodrs  17164  issubg4  17613  ghmpreima  17682  cntzsubg  17769  symgfixf1  17857  islmodd  18869  lssvsubcl  18944  lssvscl  18955  lmhmf1o  19046  pwsdiaglmhm  19057  lmimco  20183  scmatghm  20339  scmatmhm  20340  mat2pmatscmxcl  20545  fctop  20808  cctop  20810  opnneissb  20918  pnrmopn  21147  hausnei2  21157  neitx  21410  txcnmpt  21427  txrest  21434  tx1stc  21453  fbssfi  21641  opnfbas  21646  rnelfmlem  21756  alexsubALTlem3  21853  metcnp3  22345  cncfmet  22711  evth  22758  caucfil  23081  ovolun  23267  dveflem  23742  efnnfsumcl  24829  efchtdvds  24885  lgsdir2  25055  axdimuniq  25793  axcontlem2  25845  frgrwopreglem5lem  27184  frgrwopreglem5ALT  27186  friendship  27257  hvsub4  27894  his35  27945  shscli  28176  5oalem2  28514  3oalem2  28522  hosub4  28672  hmops  28879  hmopm  28880  hmopco  28882  adjmul  28951  adjadd  28952  mdslmd1lem1  29184  mdslmd1lem2  29185  elmrsubrn  31417  dfon2lem6  31693  funline  32249  neibastop2lem  32355  isbasisrelowllem1  33203  isbasisrelowllem2  33204  mbfposadd  33457  itg2addnc  33464  fdc  33541  seqpo  33543  ismtyval  33599  paddss12  35105  mzpcompact2lem  37314  jm2.26  37569  fmtnofac2lem  41480  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  zlmodzxzsubm  42137  ltsubaddb  42304  ltsubsubb  42305