Theorem ad2ant2l 759

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  funcnvqp  6604  mpteqb  7013  soxp  8141  oaass  8569  nadd42  8709  naddel12  8710  undifixp  8962  xpdom2  9091  tcrank  9901  elhf3OLD  9923  inawinalem  10774  addcanpr  11131  ltsosr  11179  1re  11308  add42  11532  muladd  11748  mulsub  11759  divmuleq  12022  ltmul12a  12173  lemul12b  12174  lemul12a  12175  mulge0b  12187  qaddcl  13093  qmulcl  13095  iooshf  13557  fzass4  13696  elfzomelpfzo  13907  modid  14036  swrdccatin2  14878  pfxccatin12  14882  cshwleneq  14968  s2eq2seq  15088  tanaddlem  16334  fpwipodrs  18714  gsumsgrpccat  19036  issubg4  19356  ghmpreima  19452  cntzsubg  19553  symgfixf1  19651  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  rhmsubcrngclem2  20919  islmodd  21141  lssvsubcl  21219  lssvscl  21230  lmhmf1o  21321  pwsdiaglmhm  21332  lmimco  22150  scmatghm  22848  scmatmhm  22849  mat2pmatscmxcl  23058  fctop  23322  cctop  23324  opnneissb  23432  pnrmopn  23661  hausnei2  23671  neitx  23926  txcnmpt  23943  txrest  23950  tx1stc  23969  fbssfi  24156  opnfbas  24161  rnelfmlem  24271  alexsubALTlem3  24368  metcnp3  24859  cncfmet  25230  evth  25280  caucfil  25604  ovolun  25820  dveflem  26299  efnnfsumcl  27430  efchtdvds  27486  lgsdir2  27657  precsexlem11  28603  axdimuniq  29491  axcontlem2  29543  clwwlkf1  30640  frgrwopreglem5lem  30921  frgrwopreglem5ALT  30923  friendship  31000  hvsub4  31639  his35  31690  shscli  31919  5oalem2  32257  3oalem2  32265  hosub4  32415  hmops  32622  hmopm  32623  hmopco  32625  adjmul  32694  adjadd  32695  mdslmd1lem1  32927  mdslmd1lem2  32928  noinfepfnregs  35800  satffunlem  36166  elmrsubrn  36285  dfon2lem6  36550  funline  36907  nmulprop  36939  nmulel1  36964  neibastop2lem  37148  isbasisrelowllem1  38278  isbasisrelowllem2  38279  mbfposadd  38585  itg2addnc  38592  fdc  38679  seqpo  38681  ismtyval  38734  paddss12  40876  zaddcom  43528  zmulcom  43532  mzpcompact2lem  43761  jm2.26  44008  orddif0suc  44269  tfsconcatun  44338  oaun3lem2  44376  fmtnofac2lem  48652  isubgrgrim  49026  zlmodzxzsubm  49470  ltsubaddb  49625  ltsubsubb  49626