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  6630  mpteqb  7035  soxp  8154  wfrlem4OLD  8352  oaass  8599  nadd42  8737  naddel12  8738  undifixp  8974  undomOLD  9100  xpdom2  9107  tcrank  9924  inawinalem  10729  addcanpr  11086  ltsosr  11134  1re  11261  add42  11483  muladd  11695  mulsub  11706  divmuleq  11972  ltmul12a  12123  lemul12b  12124  lemul12a  12125  mulge0b  12138  qaddcl  13007  qmulcl  13009  iooshf  13466  fzass4  13602  elfzomelpfzo  13810  modid  13936  swrdccatin2  14767  pfxccatin12  14771  cshwleneq  14855  s2eq2seq  14976  tanaddlem  16202  fpwipodrs  18585  gsumsgrpccat  18853  issubg4  19163  ghmpreima  19256  cntzsubg  19357  symgfixf1  19455  rnghmsubcsetclem2  20632  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  islmodd  20864  lssvsubcl  20942  lssvscl  20953  lmhmf1o  21045  pwsdiaglmhm  21056  lmimco  21864  scmatghm  22539  scmatmhm  22540  mat2pmatscmxcl  22746  fctop  23011  cctop  23013  opnneissb  23122  pnrmopn  23351  hausnei2  23361  neitx  23615  txcnmpt  23632  txrest  23639  tx1stc  23658  fbssfi  23845  opnfbas  23850  rnelfmlem  23960  alexsubALTlem3  24057  metcnp3  24553  cncfmet  24935  evth  24991  caucfil  25317  ovolun  25534  dveflem  26017  efnnfsumcl  27146  efchtdvds  27202  lgsdir2  27374  precsexlem11  28241  axdimuniq  28928  axcontlem2  28980  clwwlkf1  30068  frgrwopreglem5lem  30339  frgrwopreglem5ALT  30341  friendship  30418  hvsub4  31056  his35  31107  shscli  31336  5oalem2  31674  3oalem2  31682  hosub4  31832  hmops  32039  hmopm  32040  hmopco  32042  adjmul  32111  adjadd  32112  mdslmd1lem1  32344  mdslmd1lem2  32345  satffunlem  35406  elmrsubrn  35525  dfon2lem6  35789  funline  36143  neibastop2lem  36361  isbasisrelowllem1  37356  isbasisrelowllem2  37357  mbfposadd  37674  itg2addnc  37681  fdc  37752  seqpo  37754  ismtyval  37807  paddss12  39821  zaddcom  42482  zmulcom  42486  mzpcompact2lem  42762  jm2.26  43014  orddif0suc  43281  tfsconcatun  43350  oaun3lem2  43388  fmtnofac2lem  47555  isubgrgrim  47897  zlmodzxzsubm  48275  ltsubaddb  48431  ltsubsubb  48432