Theorem ad2ant2rl 747

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 714	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 713	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  poseq  8163  omwordri  8593  omxpenlem  9098  infxpabs  10237  domfin4  10336  isf32lem7  10384  ordpipq  10967  muladd  11678  lemul12b  12104  mulge0b  12117  qaddcl  12982  iooshf  13438  elfzomelpfzo  13772  expnegz  14097  swrdccatin1  14711  bitsshft  16453  setscom  17152  lubun  18510  grplmulf1o  18977  grpraddf1o  18978  srhmsubc  20625  lmodfopne  20795  lidl1el  21134  frlmipval  21730  en2top  22932  cnpnei  23212  kgenidm  23495  ufileu  23867  fmfnfmlem4  23905  isngp4  24565  fsumcn  24832  evth  24929  cmslssbn  25344  mbfmulc2lem  25620  itg1addlem4  25672  itg1addlem4OLD  25673  dgreq0  26245  cxplt3  26679  cxple3  26680  basellem4  27061  sltsolem1  27654  nodenselem7  27669  axcontlem2  28848  umgr2edg  29094  nbumgrvtx  29231  clwwlkf1  29931  umgrhashecclwwlk  29960  frgrncvvdeqlem9  30189  frgrwopreglem5ALT  30204  numclwwlk7lem  30271  grpoidinvlem3  30388  grpoideu  30391  grporcan  30400  3oalem2  31545  hmops  31902  adjadd  31975  mdslmd4i  32215  mdexchi  32217  mdsymlem1  32285  bnj607  34678  cvxsconn  34984  tailfb  35992  lindsadd  37217  poimirlem14  37238  mblfinlem4  37264  ismblfin  37265  ismtyres  37412  ghomco  37495  rngoisocnv  37585  1idl  37630  ps-2  39081  cfsetsnfsetf1  46579  srhmsubcALTV  47573  aacllem  48420