Theorem ad2ant2l 742

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 712	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 710	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 206  df-an 396

This theorem is referenced by:  funcnvqp  6482  mpteqb  6876  mpofunOLD  7377  soxp  7941  wfrlem4OLD  8114  oaass  8354  undifixp  8680  undom  8800  xpdom2  8807  tcrank  9573  inawinalem  10376  addcanpr  10733  ltsosr  10781  1re  10906  add42  11126  muladd  11337  mulsub  11348  divmuleq  11610  ltmul12a  11761  lemul12b  11762  lemul12a  11763  mulge0b  11775  qaddcl  12634  qmulcl  12636  iooshf  13087  fzass4  13223  elfzomelpfzo  13419  modid  13544  swrdccatin2  14370  pfxccatin12  14374  cshwleneq  14458  s2eq2seq  14578  tanaddlem  15803  fpwipodrs  18173  gsumsgrpccat  18393  issubg4  18689  ghmpreima  18771  cntzsubg  18858  symgfixf1  18960  islmodd  20044  lssvsubcl  20120  lssvscl  20132  lmhmf1o  20223  pwsdiaglmhm  20234  lmimco  20961  scmatghm  21590  scmatmhm  21591  mat2pmatscmxcl  21797  fctop  22062  cctop  22064  opnneissb  22173  pnrmopn  22402  hausnei2  22412  neitx  22666  txcnmpt  22683  txrest  22690  tx1stc  22709  fbssfi  22896  opnfbas  22901  rnelfmlem  23011  alexsubALTlem3  23108  metcnp3  23602  cncfmet  23978  evth  24028  caucfil  24352  ovolun  24568  dveflem  25048  efnnfsumcl  26157  efchtdvds  26213  lgsdir2  26383  axdimuniq  27184  axcontlem2  27236  clwwlkf1  28314  frgrwopreglem5lem  28585  frgrwopreglem5ALT  28587  friendship  28664  hvsub4  29300  his35  29351  shscli  29580  5oalem2  29918  3oalem2  29926  hosub4  30076  hmops  30283  hmopm  30284  hmopco  30286  adjmul  30355  adjadd  30356  mdslmd1lem1  30588  mdslmd1lem2  30589  satffunlem  33263  elmrsubrn  33382  dfon2lem6  33670  funline  34371  neibastop2lem  34476  isbasisrelowllem1  35453  isbasisrelowllem2  35454  mbfposadd  35751  itg2addnc  35758  fdc  35830  seqpo  35832  ismtyval  35885  paddss12  37760  mzpcompact2lem  40489  jm2.26  40740  fmtnofac2lem  44908  rnghmsubcsetclem2  45422  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  zlmodzxzsubm  45583  ltsubaddb  45743  ltsubsubb  45744