Theorem ad2ant2l 746

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

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2l	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 714	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  funcnvqp  6583  mpteqb  6990  soxp  8111  oaass  8528  nadd42  8666  naddel12  8667  undifixp  8910  undomOLD  9034  xpdom2  9041  tcrank  9844  inawinalem  10649  addcanpr  11006  ltsosr  11054  1re  11181  add42  11403  muladd  11617  mulsub  11628  divmuleq  11894  ltmul12a  12045  lemul12b  12046  lemul12a  12047  mulge0b  12060  qaddcl  12931  qmulcl  12933  iooshf  13394  fzass4  13530  elfzomelpfzo  13739  modid  13865  swrdccatin2  14701  pfxccatin12  14705  cshwleneq  14789  s2eq2seq  14910  tanaddlem  16141  fpwipodrs  18506  gsumsgrpccat  18774  issubg4  19084  ghmpreima  19177  cntzsubg  19278  symgfixf1  19374  rnghmsubcsetclem2  20548  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  islmodd  20779  lssvsubcl  20857  lssvscl  20868  lmhmf1o  20960  pwsdiaglmhm  20971  lmimco  21760  scmatghm  22427  scmatmhm  22428  mat2pmatscmxcl  22634  fctop  22898  cctop  22900  opnneissb  23008  pnrmopn  23237  hausnei2  23247  neitx  23501  txcnmpt  23518  txrest  23525  tx1stc  23544  fbssfi  23731  opnfbas  23736  rnelfmlem  23846  alexsubALTlem3  23943  metcnp3  24435  cncfmet  24809  evth  24865  caucfil  25190  ovolun  25407  dveflem  25890  efnnfsumcl  27020  efchtdvds  27076  lgsdir2  27248  precsexlem11  28126  axdimuniq  28847  axcontlem2  28899  clwwlkf1  29985  frgrwopreglem5lem  30256  frgrwopreglem5ALT  30258  friendship  30335  hvsub4  30973  his35  31024  shscli  31253  5oalem2  31591  3oalem2  31599  hosub4  31749  hmops  31956  hmopm  31957  hmopco  31959  adjmul  32028  adjadd  32029  mdslmd1lem1  32261  mdslmd1lem2  32262  satffunlem  35395  elmrsubrn  35514  dfon2lem6  35783  funline  36137  neibastop2lem  36355  isbasisrelowllem1  37350  isbasisrelowllem2  37351  mbfposadd  37668  itg2addnc  37675  fdc  37746  seqpo  37748  ismtyval  37801  paddss12  39820  zaddcom  42459  zmulcom  42463  mzpcompact2lem  42746  jm2.26  42998  orddif0suc  43264  tfsconcatun  43333  oaun3lem2  43371  fmtnofac2lem  47573  isubgrgrim  47933  zlmodzxzsubm  48351  ltsubaddb  48507  ltsubsubb  48508