Theorem ad2ant2rl 750

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 716	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  8102  omwordri  8501  omxpenlem  9010  infxpabs  10127  domfin4  10227  isf32lem7  10275  ordpipq  10859  muladd  11576  lemul12b  12006  mulge0b  12020  qaddcl  12909  iooshf  13373  elfzomelpfzo  13721  expnegz  14052  swrdccatin1  14681  bitsshft  16438  setscom  17144  lubun  18475  grplmulf1o  18983  grpraddf1o  18984  srhmsubc  20651  lmodfopne  20889  lidl1el  21219  frlmipval  21772  en2top  22963  cnpnei  23242  kgenidm  23525  ufileu  23897  fmfnfmlem4  23935  isngp4  24590  fsumcn  24850  evth  24939  cmslssbn  25352  mbfmulc2lem  25627  itg1addlem4  25679  dgreq0  26243  cxplt3  26680  cxple3  26681  basellem4  27064  ltssolem1  27656  nodenselem7  27671  zmulscld  28406  axcontlem2  29051  umgr2edg  29295  nbumgrvtx  29432  clwwlkf1  30137  umgrhashecclwwlk  30166  frgrncvvdeqlem9  30395  frgrwopreglem5ALT  30410  numclwwlk7lem  30477  grpoidinvlem3  30595  grpoideu  30598  grporcan  30607  3oalem2  31752  hmops  32109  adjadd  32182  mdslmd4i  32422  mdexchi  32424  mdsymlem1  32492  bnj607  35077  cvxsconn  35444  tailfb  36578  lindsadd  37951  poimirlem14  37972  mblfinlem4  37998  ismblfin  37999  ismtyres  38146  ghomco  38229  rngoisocnv  38319  1idl  38364  ps-2  39941  cfsetsnfsetf1  47522  usgrgrtrirex  48441  grlictr  48506  gpgvtx0  48544  srhmsubcALTV  48816  aacllem  50291