Theorem ad2ant2l 758

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  funcnvqp  6600  mpteqb  7009  soxp  8121  oaass  8542  nadd42  8682  naddel12  8683  undifixp  8928  xpdom2  9056  tcrank  9852  inawinalem  10669  addcanpr  11026  ltsosr  11074  1re  11203  add42  11427  muladd  11641  mulsub  11652  divmuleq  11915  ltmul12a  12066  lemul12b  12067  lemul12a  12068  mulge0b  12080  qaddcl  12984  qmulcl  12986  iooshf  13448  fzass4  13586  elfzomelpfzo  13797  modid  13925  swrdccatin2  14762  pfxccatin12  14766  cshwleneq  14850  s2eq2seq  14970  tanaddlem  16217  fpwipodrs  18591  gsumsgrpccat  18894  issubg4  19207  ghmpreima  19303  cntzsubg  19404  symgfixf1  19502  rnghmsubcsetclem2  20731  rhmsubcsetclem2  20760  rhmsubcrngclem2  20766  islmodd  20987  lssvsubcl  21065  lssvscl  21076  lmhmf1o  21167  pwsdiaglmhm  21178  lmimco  21994  scmatghm  22690  scmatmhm  22691  mat2pmatscmxcl  22897  fctop  23161  cctop  23163  opnneissb  23271  pnrmopn  23500  hausnei2  23510  neitx  23764  txcnmpt  23781  txrest  23788  tx1stc  23807  fbssfi  23994  opnfbas  23999  rnelfmlem  24109  alexsubALTlem3  24206  metcnp3  24697  cncfmet  25068  evth  25118  caucfil  25442  ovolun  25658  dveflem  26138  efnnfsumcl  27267  efchtdvds  27323  lgsdir2  27494  precsexlem11  28410  axdimuniq  29263  axcontlem2  29315  clwwlkf1  30400  frgrwopreglem5lem  30671  frgrwopreglem5ALT  30673  friendship  30750  hvsub4  31389  his35  31440  shscli  31669  5oalem2  32007  3oalem2  32015  hosub4  32165  hmops  32372  hmopm  32373  hmopco  32375  adjmul  32444  adjadd  32445  mdslmd1lem1  32677  mdslmd1lem2  32678  noinfepfnregs  35545  satffunlem  35893  elmrsubrn  36012  dfon2lem6  36278  funline  36634  nmulprop  36682  nmulel1  36707  neibastop2lem  36891  isbasisrelowllem1  38021  isbasisrelowllem2  38022  mbfposadd  38338  itg2addnc  38345  fdc  38416  seqpo  38418  ismtyval  38471  paddss12  40613  zaddcom  43258  zmulcom  43262  mzpcompact2lem  43502  jm2.26  43749  orddif0suc  44015  tfsconcatun  44084  oaun3lem2  44122  fmtnofac2lem  48340  isubgrgrim  48714  zlmodzxzsubm  49159  ltsubaddb  49314  ltsubsubb  49315