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  6556  mpteqb  6960  soxp  8071  oaass  8488  nadd42  8627  naddel12  8628  undifixp  8872  xpdom2  9000  tcrank  9796  inawinalem  10600  addcanpr  10957  ltsosr  11005  1re  11132  add42  11355  muladd  11569  mulsub  11580  divmuleq  11846  ltmul12a  11997  lemul12b  11998  lemul12a  11999  mulge0b  12012  qaddcl  12878  qmulcl  12880  iooshf  13342  fzass4  13478  elfzomelpfzo  13688  modid  13816  swrdccatin2  14652  pfxccatin12  14656  cshwleneq  14740  s2eq2seq  14860  tanaddlem  16091  fpwipodrs  18463  gsumsgrpccat  18765  issubg4  19075  ghmpreima  19167  cntzsubg  19268  symgfixf1  19366  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  islmodd  20817  lssvsubcl  20895  lssvscl  20906  lmhmf1o  20998  pwsdiaglmhm  21009  lmimco  21799  scmatghm  22477  scmatmhm  22478  mat2pmatscmxcl  22684  fctop  22948  cctop  22950  opnneissb  23058  pnrmopn  23287  hausnei2  23297  neitx  23551  txcnmpt  23568  txrest  23575  tx1stc  23594  fbssfi  23781  opnfbas  23786  rnelfmlem  23896  alexsubALTlem3  23993  metcnp3  24484  cncfmet  24858  evth  24914  caucfil  25239  ovolun  25456  dveflem  25939  efnnfsumcl  27069  efchtdvds  27125  lgsdir2  27297  precsexlem11  28213  axdimuniq  28986  axcontlem2  29038  clwwlkf1  30124  frgrwopreglem5lem  30395  frgrwopreglem5ALT  30397  friendship  30474  hvsub4  31112  his35  31163  shscli  31392  5oalem2  31730  3oalem2  31738  hosub4  31888  hmops  32095  hmopm  32096  hmopco  32098  adjmul  32167  adjadd  32168  mdslmd1lem1  32400  mdslmd1lem2  32401  noinfepfnregs  35288  satffunlem  35595  elmrsubrn  35714  dfon2lem6  35980  funline  36336  neibastop2lem  36554  isbasisrelowllem1  37560  isbasisrelowllem2  37561  mbfposadd  37868  itg2addnc  37875  fdc  37946  seqpo  37948  ismtyval  38001  paddss12  40089  zaddcom  42729  zmulcom  42733  mzpcompact2lem  43003  jm2.26  43254  orddif0suc  43520  tfsconcatun  43589  oaun3lem2  43627  fmtnofac2lem  47824  isubgrgrim  48185  zlmodzxzsubm  48615  ltsubaddb  48770  ltsubsubb  48771