Theorem ad2ant2l 742

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 712	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 710	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  funcnvqp  6611  mpteqb  7016  mpofunOLD  7535  soxp  8117  wfrlem4OLD  8314  oaass  8563  nadd42  8700  naddel12  8701  undifixp  8930  undomOLD  9062  xpdom2  9069  tcrank  9881  inawinalem  10686  addcanpr  11043  ltsosr  11091  1re  11218  add42  11439  muladd  11650  mulsub  11661  divmuleq  11923  ltmul12a  12074  lemul12b  12075  lemul12a  12076  mulge0b  12088  qaddcl  12953  qmulcl  12955  iooshf  13407  fzass4  13543  elfzomelpfzo  13740  modid  13865  swrdccatin2  14683  pfxccatin12  14687  cshwleneq  14771  s2eq2seq  14892  tanaddlem  16113  fpwipodrs  18497  gsumsgrpccat  18757  issubg4  19061  ghmpreima  19152  cntzsubg  19244  symgfixf1  19346  islmodd  20620  lssvsubcl  20698  lssvscl  20710  lmhmf1o  20801  pwsdiaglmhm  20812  lmimco  21618  scmatghm  22255  scmatmhm  22256  mat2pmatscmxcl  22462  fctop  22727  cctop  22729  opnneissb  22838  pnrmopn  23067  hausnei2  23077  neitx  23331  txcnmpt  23348  txrest  23355  tx1stc  23374  fbssfi  23561  opnfbas  23566  rnelfmlem  23676  alexsubALTlem3  23773  metcnp3  24269  cncfmet  24649  evth  24705  caucfil  25031  ovolun  25248  dveflem  25731  efnnfsumcl  26843  efchtdvds  26899  lgsdir2  27069  precsexlem11  27902  axdimuniq  28438  axcontlem2  28490  clwwlkf1  29569  frgrwopreglem5lem  29840  frgrwopreglem5ALT  29842  friendship  29919  hvsub4  30557  his35  30608  shscli  30837  5oalem2  31175  3oalem2  31183  hosub4  31333  hmops  31540  hmopm  31541  hmopco  31543  adjmul  31612  adjadd  31613  mdslmd1lem1  31845  mdslmd1lem2  31846  satffunlem  34690  elmrsubrn  34809  dfon2lem6  35064  funline  35418  neibastop2lem  35548  isbasisrelowllem1  36539  isbasisrelowllem2  36540  mbfposadd  36838  itg2addnc  36845  fdc  36916  seqpo  36918  ismtyval  36971  paddss12  38993  zaddcom  41627  zmulcom  41631  mzpcompact2lem  41791  jm2.26  42043  orddif0suc  42320  tfsconcatun  42389  oaun3lem2  42427  fmtnofac2lem  46534  rnghmsubcsetclem2  46962  rhmsubcsetclem2  47008  rhmsubcrngclem2  47014  zlmodzxzsubm  47123  ltsubaddb  47282  ltsubsubb  47283