Theorem ad2ant2l 744

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  funcnvqp  6413  mpteqb  6782  mpofun  7270  soxp  7817  wfrlem4  7952  oaass  8181  undifixp  8492  undom  8599  xpdom2  8606  tcrank  9307  inawinalem  10105  addcanpr  10462  ltsosr  10510  1re  10635  add42  10855  muladd  11066  mulsub  11077  divmuleq  11339  ltmul12a  11490  lemul12b  11491  lemul12a  11492  mulge0b  11504  qaddcl  12358  qmulcl  12360  iooshf  12809  fzass4  12939  elfzomelpfzo  13135  modid  13258  swrdccatin2  14085  pfxccatin12  14089  cshwleneq  14173  s2eq2seq  14293  tanaddlem  15513  fpwipodrs  17768  gsumsgrpccat  17998  issubg4  18292  ghmpreima  18374  cntzsubg  18461  symgfixf1  18559  islmodd  19634  lssvsubcl  19709  lssvscl  19721  lmhmf1o  19812  pwsdiaglmhm  19823  lmimco  20982  scmatghm  21136  scmatmhm  21137  mat2pmatscmxcl  21342  fctop  21606  cctop  21608  opnneissb  21716  pnrmopn  21945  hausnei2  21955  neitx  22209  txcnmpt  22226  txrest  22233  tx1stc  22252  fbssfi  22439  opnfbas  22444  rnelfmlem  22554  alexsubALTlem3  22651  metcnp3  23144  cncfmet  23510  evth  23557  caucfil  23880  ovolun  24094  dveflem  24570  efnnfsumcl  25674  efchtdvds  25730  lgsdir2  25900  axdimuniq  26693  axcontlem2  26745  clwwlkf1  27822  frgrwopreglem5lem  28093  frgrwopreglem5ALT  28095  friendship  28172  hvsub4  28808  his35  28859  shscli  29088  5oalem2  29426  3oalem2  29434  hosub4  29584  hmops  29791  hmopm  29792  hmopco  29794  adjmul  29863  adjadd  29864  mdslmd1lem1  30096  mdslmd1lem2  30097  satffunlem  32643  elmrsubrn  32762  dfon2lem6  33028  funline  33598  neibastop2lem  33703  isbasisrelowllem1  34630  isbasisrelowllem2  34631  mbfposadd  34933  itg2addnc  34940  fdc  35014  seqpo  35016  ismtyval  35072  paddss12  36949  mzpcompact2lem  39341  jm2.26  39592  fmtnofac2lem  43723  rnghmsubcsetclem2  44240  rhmsubcsetclem2  44286  rhmsubcrngclem2  44292  zlmodzxzsubm  44400  ltsubaddb  44562  ltsubsubb  44563