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  6598  mpteqb  7007  soxp  8128  oaass  8549  nadd42  8689  naddel12  8690  undifixp  8942  xpdom2  9071  tcrank  9867  inawinalem  10699  addcanpr  11056  ltsosr  11104  1re  11233  add42  11457  muladd  11671  mulsub  11682  divmuleq  11945  ltmul12a  12096  lemul12b  12097  lemul12a  12098  mulge0b  12110  qaddcl  13016  qmulcl  13018  iooshf  13480  fzass4  13618  elfzomelpfzo  13829  modid  13958  swrdccatin2  14799  pfxccatin12  14803  cshwleneq  14889  s2eq2seq  15009  tanaddlem  16255  fpwipodrs  18629  gsumsgrpccat  18950  issubg4  19270  ghmpreima  19366  cntzsubg  19467  symgfixf1  19565  rnghmsubcsetclem2  20795  rhmsubcsetclem2  20824  rhmsubcrngclem2  20830  islmodd  21051  lssvsubcl  21129  lssvscl  21140  lmhmf1o  21231  pwsdiaglmhm  21242  lmimco  22058  scmatghm  22756  scmatmhm  22757  mat2pmatscmxcl  22966  fctop  23230  cctop  23232  opnneissb  23340  pnrmopn  23569  hausnei2  23579  neitx  23834  txcnmpt  23851  txrest  23858  tx1stc  23877  fbssfi  24064  opnfbas  24069  rnelfmlem  24179  alexsubALTlem3  24276  metcnp3  24767  cncfmet  25138  evth  25188  caucfil  25512  ovolun  25728  dveflem  26207  efnnfsumcl  27340  efchtdvds  27396  lgsdir2  27567  precsexlem11  28483  axdimuniq  29371  axcontlem2  29423  clwwlkf1  30520  frgrwopreglem5lem  30801  frgrwopreglem5ALT  30803  friendship  30880  hvsub4  31519  his35  31570  shscli  31799  5oalem2  32137  3oalem2  32145  hosub4  32295  hmops  32502  hmopm  32503  hmopco  32505  adjmul  32574  adjadd  32575  mdslmd1lem1  32807  mdslmd1lem2  32808  noinfepfnregs  35659  satffunlem  35981  elmrsubrn  36100  dfon2lem6  36366  funline  36723  nmulprop  36771  nmulel1  36796  neibastop2lem  36980  isbasisrelowllem1  38110  isbasisrelowllem2  38111  mbfposadd  38417  itg2addnc  38424  fdc  38496  seqpo  38498  ismtyval  38551  paddss12  40693  zaddcom  43353  zmulcom  43357  mzpcompact2lem  43597  jm2.26  43844  orddif0suc  44110  tfsconcatun  44179  oaun3lem2  44217  fmtnofac2lem  48472  isubgrgrim  48846  zlmodzxzsubm  49290  ltsubaddb  49445  ltsubsubb  49446