Theorem ad2ant2l 746

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

This theorem is referenced by:  funcnvqp  6545  mpteqb  6948  soxp  8059  oaass  8476  nadd42  8614  naddel12  8615  undifixp  8858  xpdom2  8985  tcrank  9777  inawinalem  10580  addcanpr  10937  ltsosr  10985  1re  11112  add42  11335  muladd  11549  mulsub  11560  divmuleq  11826  ltmul12a  11977  lemul12b  11978  lemul12a  11979  mulge0b  11992  qaddcl  12863  qmulcl  12865  iooshf  13326  fzass4  13462  elfzomelpfzo  13672  modid  13800  swrdccatin2  14636  pfxccatin12  14640  cshwleneq  14724  s2eq2seq  14844  tanaddlem  16075  fpwipodrs  18446  gsumsgrpccat  18748  issubg4  19058  ghmpreima  19150  cntzsubg  19251  symgfixf1  19349  rnghmsubcsetclem2  20547  rhmsubcsetclem2  20576  rhmsubcrngclem2  20582  islmodd  20799  lssvsubcl  20877  lssvscl  20888  lmhmf1o  20980  pwsdiaglmhm  20991  lmimco  21781  scmatghm  22448  scmatmhm  22449  mat2pmatscmxcl  22655  fctop  22919  cctop  22921  opnneissb  23029  pnrmopn  23258  hausnei2  23268  neitx  23522  txcnmpt  23539  txrest  23546  tx1stc  23565  fbssfi  23752  opnfbas  23757  rnelfmlem  23867  alexsubALTlem3  23964  metcnp3  24455  cncfmet  24829  evth  24885  caucfil  25210  ovolun  25427  dveflem  25910  efnnfsumcl  27040  efchtdvds  27096  lgsdir2  27268  precsexlem11  28155  axdimuniq  28891  axcontlem2  28943  clwwlkf1  30029  frgrwopreglem5lem  30300  frgrwopreglem5ALT  30302  friendship  30379  hvsub4  31017  his35  31068  shscli  31297  5oalem2  31635  3oalem2  31643  hosub4  31793  hmops  32000  hmopm  32001  hmopco  32003  adjmul  32072  adjadd  32073  mdslmd1lem1  32305  mdslmd1lem2  32306  satffunlem  35445  elmrsubrn  35564  dfon2lem6  35830  funline  36186  neibastop2lem  36404  isbasisrelowllem1  37399  isbasisrelowllem2  37400  mbfposadd  37717  itg2addnc  37724  fdc  37795  seqpo  37797  ismtyval  37850  paddss12  39928  zaddcom  42567  zmulcom  42571  mzpcompact2lem  42854  jm2.26  43105  orddif0suc  43371  tfsconcatun  43440  oaun3lem2  43478  fmtnofac2lem  47678  isubgrgrim  48039  zlmodzxzsubm  48469  ltsubaddb  48625  ltsubsubb  48626