Theorem ad2ant2rl 755

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  poseq  8098  omwordri  8497  omxpenlem  9006  infxpabs  10124  domfin4  10224  isf32lem7  10272  ordpipq  10856  muladd  11573  lemul12b  12003  mulge0b  12017  qaddcl  12906  iooshf  13370  elfzomelpfzo  13718  expnegz  14049  swrdccatin1  14678  bitsshft  16435  setscom  17141  lubun  18472  grplmulf1o  18980  grpraddf1o  18981  srhmsubc  20652  lmodfopne  20890  lidl1el  21219  frlmipval  21754  en2top  22968  cnpnei  23247  kgenidm  23530  ufileu  23902  fmfnfmlem4  23940  isngp4  24595  fsumcn  24855  evth  24944  cmslssbn  25357  mbfmulc2lem  25632  itg1addlem4  25684  dgreq0  26248  cxplt3  26682  cxple3  26683  basellem4  27065  ltssolem1  27657  nodenselem7  27672  zmulscld  28407  axcontlem2  29052  umgr2edg  29296  nbumgrvtx  29433  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  35098  cvxsconn  35471  tailfb  36605  lindsadd  37980  poimirlem14  38001  mblfinlem4  38027  ismblfin  38028  ismtyres  38175  ghomco  38258  rngoisocnv  38348  1idl  38393  ps-2  39970  cfsetsnfsetf1  47522  usgrgrtrirex  48441  grlictr  48506  gpgvtx0  48544  srhmsubcALTV  48816  aacllem  50291