Theorem ad2ant2rl 761

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  poseq  8154  omwordri  8557  omxpenlem  9066  infxpabs  10194  domfin4  10295  isf32lem7  10343  ordpipq  10927  muladd  11646  lemul12b  12072  mulge0b  12085  qaddcl  12989  iooshf  13453  elfzomelpfzo  13801  expnegz  14132  swrdccatin1  14762  bitsshft  16533  setscom  17240  lubun  18571  grplmulf1o  19079  grpraddf1o  19080  srhmsubc  20765  lmodfopne  20999  lidl1el  21329  frlmipval  21898  en2top  23111  cnpnei  23390  kgenidm  23673  ufileu  24045  fmfnfmlem4  24083  isngp4  24738  fsumcn  24998  evth  25087  cmslssbn  25500  mbfmulc2lem  25775  itg1addlem4  25827  dgreq0  26391  cxplt3  26831  cxple3  26832  basellem4  27214  ltssolem1  27805  nodenselem7  27820  zmulscld  28556  axcontlem2  29256  umgr2edg  29500  nbumgrvtx  29637  clwwlkf1  30341  umgrhashecclwwlk  30370  frgrncvvdeqlem9  30599  frgrwopreglem5ALT  30614  numclwwlk7lem  30681  grpoidinvlem3  30799  grpoideu  30802  grporcan  30811  3oalem2  31956  hmops  32313  adjadd  32386  mdslmd4i  32626  mdexchi  32628  mdsymlem1  32696  bnj607  35249  cvxsconn  35668  tailfb  36811  lindsadd  38186  poimirlem14  38207  mblfinlem4  38233  ismblfin  38234  ismtyres  38381  ghomco  38464  rngoisocnv  38554  1idl  38599  ps-2  40176  cfsetsnfsetf1  47719  usgrgrtrirex  48638  grlictr  48703  gpgvtx0  48741  srhmsubcALTV  49013  aacllem  50509