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  6564  mpteqb  6969  soxp  8085  oaass  8502  nadd42  8640  naddel12  8641  undifixp  8884  xpdom2  9013  tcrank  9813  inawinalem  10618  addcanpr  10975  ltsosr  11023  1re  11150  add42  11372  muladd  11586  mulsub  11597  divmuleq  11863  ltmul12a  12014  lemul12b  12015  lemul12a  12016  mulge0b  12029  qaddcl  12900  qmulcl  12902  iooshf  13363  fzass4  13499  elfzomelpfzo  13708  modid  13834  swrdccatin2  14670  pfxccatin12  14674  cshwleneq  14758  s2eq2seq  14879  tanaddlem  16110  fpwipodrs  18481  gsumsgrpccat  18749  issubg4  19059  ghmpreima  19152  cntzsubg  19253  symgfixf1  19351  rnghmsubcsetclem2  20552  rhmsubcsetclem2  20581  rhmsubcrngclem2  20587  islmodd  20804  lssvsubcl  20882  lssvscl  20893  lmhmf1o  20985  pwsdiaglmhm  20996  lmimco  21786  scmatghm  22453  scmatmhm  22454  mat2pmatscmxcl  22660  fctop  22924  cctop  22926  opnneissb  23034  pnrmopn  23263  hausnei2  23273  neitx  23527  txcnmpt  23544  txrest  23551  tx1stc  23570  fbssfi  23757  opnfbas  23762  rnelfmlem  23872  alexsubALTlem3  23969  metcnp3  24461  cncfmet  24835  evth  24891  caucfil  25216  ovolun  25433  dveflem  25916  efnnfsumcl  27046  efchtdvds  27102  lgsdir2  27274  precsexlem11  28159  axdimuniq  28893  axcontlem2  28945  clwwlkf1  30028  frgrwopreglem5lem  30299  frgrwopreglem5ALT  30301  friendship  30378  hvsub4  31016  his35  31067  shscli  31296  5oalem2  31634  3oalem2  31642  hosub4  31792  hmops  31999  hmopm  32000  hmopco  32002  adjmul  32071  adjadd  32072  mdslmd1lem1  32304  mdslmd1lem2  32305  satffunlem  35381  elmrsubrn  35500  dfon2lem6  35769  funline  36123  neibastop2lem  36341  isbasisrelowllem1  37336  isbasisrelowllem2  37337  mbfposadd  37654  itg2addnc  37661  fdc  37732  seqpo  37734  ismtyval  37787  paddss12  39806  zaddcom  42445  zmulcom  42449  mzpcompact2lem  42732  jm2.26  42984  orddif0suc  43250  tfsconcatun  43319  oaun3lem2  43357  fmtnofac2lem  47562  isubgrgrim  47922  zlmodzxzsubm  48340  ltsubaddb  48496  ltsubsubb  48497