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  8137  omwordri  8536  omxpenlem  9042  infxpabs  10164  domfin4  10264  isf32lem7  10312  ordpipq  10895  muladd  11610  lemul12b  12039  mulge0b  12053  qaddcl  12924  iooshf  13387  elfzomelpfzo  13732  expnegz  14061  swrdccatin1  14690  bitsshft  16445  setscom  17150  lubun  18474  grplmulf1o  18945  grpraddf1o  18946  srhmsubc  20589  lmodfopne  20806  lidl1el  21136  frlmipval  21688  en2top  22872  cnpnei  23151  kgenidm  23434  ufileu  23806  fmfnfmlem4  23844  isngp4  24500  fsumcn  24761  evth  24858  cmslssbn  25272  mbfmulc2lem  25548  itg1addlem4  25600  dgreq0  26171  cxplt3  26609  cxple3  26610  basellem4  26994  sltsolem1  27587  nodenselem7  27602  zmulscld  28285  axcontlem2  28892  umgr2edg  29136  nbumgrvtx  29273  clwwlkf1  29978  umgrhashecclwwlk  30007  frgrncvvdeqlem9  30236  frgrwopreglem5ALT  30251  numclwwlk7lem  30318  grpoidinvlem3  30435  grpoideu  30438  grporcan  30447  3oalem2  31592  hmops  31949  adjadd  32022  mdslmd4i  32262  mdexchi  32264  mdsymlem1  32332  bnj607  34906  cvxsconn  35230  tailfb  36365  lindsadd  37607  poimirlem14  37628  mblfinlem4  37654  ismblfin  37655  ismtyres  37802  ghomco  37885  rngoisocnv  37975  1idl  38020  ps-2  39472  cfsetsnfsetf1  47060  usgrgrtrirex  47949  grlictr  48007  gpgvtx0  48044  srhmsubcALTV  48313  aacllem  49790