Theorem ad2ant2rl 749

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2rl	⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2rl

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 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:  poseq  8140  omwordri  8539  omxpenlem  9047  infxpabs  10171  domfin4  10271  isf32lem7  10319  ordpipq  10902  muladd  11617  lemul12b  12046  mulge0b  12060  qaddcl  12931  iooshf  13394  elfzomelpfzo  13739  expnegz  14068  swrdccatin1  14697  bitsshft  16452  setscom  17157  lubun  18481  grplmulf1o  18952  grpraddf1o  18953  srhmsubc  20596  lmodfopne  20813  lidl1el  21143  frlmipval  21695  en2top  22879  cnpnei  23158  kgenidm  23441  ufileu  23813  fmfnfmlem4  23851  isngp4  24507  fsumcn  24768  evth  24865  cmslssbn  25279  mbfmulc2lem  25555  itg1addlem4  25607  dgreq0  26178  cxplt3  26616  cxple3  26617  basellem4  27001  sltsolem1  27594  nodenselem7  27609  zmulscld  28292  axcontlem2  28899  umgr2edg  29143  nbumgrvtx  29280  clwwlkf1  29985  umgrhashecclwwlk  30014  frgrncvvdeqlem9  30243  frgrwopreglem5ALT  30258  numclwwlk7lem  30325  grpoidinvlem3  30442  grpoideu  30445  grporcan  30454  3oalem2  31599  hmops  31956  adjadd  32029  mdslmd4i  32269  mdexchi  32271  mdsymlem1  32339  bnj607  34913  cvxsconn  35237  tailfb  36372  lindsadd  37614  poimirlem14  37635  mblfinlem4  37661  ismblfin  37662  ismtyres  37809  ghomco  37892  rngoisocnv  37982  1idl  38027  ps-2  39479  cfsetsnfsetf1  47064  usgrgrtrirex  47953  grlictr  48011  gpgvtx0  48048  srhmsubcALTV  48317  aacllem  49794