Theorem ad2ant2l 747

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 715	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  6564  mpteqb  6969  soxp  8081  oaass  8498  nadd42  8637  naddel12  8638  undifixp  8884  xpdom2  9012  tcrank  9808  inawinalem  10612  addcanpr  10969  ltsosr  11017  1re  11144  add42  11367  muladd  11581  mulsub  11592  divmuleq  11858  ltmul12a  12009  lemul12b  12010  lemul12a  12011  mulge0b  12024  qaddcl  12890  qmulcl  12892  iooshf  13354  fzass4  13490  elfzomelpfzo  13700  modid  13828  swrdccatin2  14664  pfxccatin12  14668  cshwleneq  14752  s2eq2seq  14872  tanaddlem  16103  fpwipodrs  18475  gsumsgrpccat  18777  issubg4  19087  ghmpreima  19179  cntzsubg  19280  symgfixf1  19378  rnghmsubcsetclem2  20577  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  islmodd  20829  lssvsubcl  20907  lssvscl  20918  lmhmf1o  21010  pwsdiaglmhm  21021  lmimco  21811  scmatghm  22489  scmatmhm  22490  mat2pmatscmxcl  22696  fctop  22960  cctop  22962  opnneissb  23070  pnrmopn  23299  hausnei2  23309  neitx  23563  txcnmpt  23580  txrest  23587  tx1stc  23606  fbssfi  23793  opnfbas  23798  rnelfmlem  23908  alexsubALTlem3  24005  metcnp3  24496  cncfmet  24870  evth  24926  caucfil  25251  ovolun  25468  dveflem  25951  efnnfsumcl  27081  efchtdvds  27137  lgsdir2  27309  precsexlem11  28225  axdimuniq  28998  axcontlem2  29050  clwwlkf1  30136  frgrwopreglem5lem  30407  frgrwopreglem5ALT  30409  friendship  30486  hvsub4  31125  his35  31176  shscli  31405  5oalem2  31743  3oalem2  31751  hosub4  31901  hmops  32108  hmopm  32109  hmopco  32111  adjmul  32180  adjadd  32181  mdslmd1lem1  32413  mdslmd1lem2  32414  noinfepfnregs  35310  satffunlem  35617  elmrsubrn  35736  dfon2lem6  36002  funline  36358  neibastop2lem  36576  isbasisrelowllem1  37610  isbasisrelowllem2  37611  mbfposadd  37918  itg2addnc  37925  fdc  37996  seqpo  37998  ismtyval  38051  paddss12  40195  zaddcom  42834  zmulcom  42838  mzpcompact2lem  43108  jm2.26  43359  orddif0suc  43625  tfsconcatun  43694  oaun3lem2  43732  fmtnofac2lem  47928  isubgrgrim  48289  zlmodzxzsubm  48719  ltsubaddb  48874  ltsubsubb  48875