Theorem ad2ant2l 747

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 715	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  6557  mpteqb  6962  soxp  8073  oaass  8490  nadd42  8629  naddel12  8630  undifixp  8876  xpdom2  9004  tcrank  9802  inawinalem  10606  addcanpr  10963  ltsosr  11011  1re  11138  add42  11362  muladd  11576  mulsub  11587  divmuleq  11854  ltmul12a  12005  lemul12b  12006  lemul12a  12007  mulge0b  12020  qaddcl  12909  qmulcl  12911  iooshf  13373  fzass4  13510  elfzomelpfzo  13721  modid  13849  swrdccatin2  14685  pfxccatin12  14689  cshwleneq  14773  s2eq2seq  14893  tanaddlem  16127  fpwipodrs  18500  gsumsgrpccat  18802  issubg4  19115  ghmpreima  19207  cntzsubg  19308  symgfixf1  19406  rnghmsubcsetclem2  20603  rhmsubcsetclem2  20632  rhmsubcrngclem2  20638  islmodd  20855  lssvsubcl  20933  lssvscl  20944  lmhmf1o  21036  pwsdiaglmhm  21047  lmimco  21837  scmatghm  22511  scmatmhm  22512  mat2pmatscmxcl  22718  fctop  22982  cctop  22984  opnneissb  23092  pnrmopn  23321  hausnei2  23331  neitx  23585  txcnmpt  23602  txrest  23609  tx1stc  23628  fbssfi  23815  opnfbas  23820  rnelfmlem  23930  alexsubALTlem3  24027  metcnp3  24518  cncfmet  24889  evth  24939  caucfil  25263  ovolun  25479  dveflem  25959  efnnfsumcl  27083  efchtdvds  27139  lgsdir2  27310  precsexlem11  28226  axdimuniq  28999  axcontlem2  29051  clwwlkf1  30137  frgrwopreglem5lem  30408  frgrwopreglem5ALT  30410  friendship  30487  hvsub4  31126  his35  31177  shscli  31406  5oalem2  31744  3oalem2  31752  hosub4  31902  hmops  32109  hmopm  32110  hmopco  32112  adjmul  32181  adjadd  32182  mdslmd1lem1  32414  mdslmd1lem2  32415  noinfepfnregs  35295  satffunlem  35602  elmrsubrn  35721  dfon2lem6  35987  funline  36343  neibastop2lem  36561  isbasisrelowllem1  37688  isbasisrelowllem2  37689  mbfposadd  38005  itg2addnc  38012  fdc  38083  seqpo  38085  ismtyval  38138  paddss12  40282  zaddcom  42926  zmulcom  42930  mzpcompact2lem  43200  jm2.26  43451  orddif0suc  43717  tfsconcatun  43786  oaun3lem2  43824  fmtnofac2lem  48046  isubgrgrim  48420  zlmodzxzsubm  48850  ltsubaddb  49005  ltsubsubb  49006