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  8182  omwordri  8609  omxpenlem  9112  infxpabs  10249  domfin4  10349  isf32lem7  10397  ordpipq  10980  muladd  11693  lemul12b  12122  mulge0b  12136  qaddcl  13005  iooshf  13463  elfzomelpfzo  13807  expnegz  14134  swrdccatin1  14760  bitsshft  16509  setscom  17214  lubun  18573  grplmulf1o  19044  grpraddf1o  19045  srhmsubc  20697  lmodfopne  20915  lidl1el  21254  frlmipval  21817  en2top  23008  cnpnei  23288  kgenidm  23571  ufileu  23943  fmfnfmlem4  23981  isngp4  24641  fsumcn  24908  evth  25005  cmslssbn  25420  mbfmulc2lem  25696  itg1addlem4  25748  itg1addlem4OLD  25749  dgreq0  26320  cxplt3  26757  cxple3  26758  basellem4  27142  sltsolem1  27735  nodenselem7  27750  zmulscld  28398  axcontlem2  28995  umgr2edg  29241  nbumgrvtx  29378  clwwlkf1  30078  umgrhashecclwwlk  30107  frgrncvvdeqlem9  30336  frgrwopreglem5ALT  30351  numclwwlk7lem  30418  grpoidinvlem3  30535  grpoideu  30538  grporcan  30547  3oalem2  31692  hmops  32049  adjadd  32122  mdslmd4i  32362  mdexchi  32364  mdsymlem1  32432  bnj607  34909  cvxsconn  35228  tailfb  36360  lindsadd  37600  poimirlem14  37621  mblfinlem4  37647  ismblfin  37648  ismtyres  37795  ghomco  37878  rngoisocnv  37968  1idl  38013  ps-2  39461  cfsetsnfsetf1  47009  usgrgrtrirex  47853  grlictr  47911  gpgvtx0  47944  srhmsubcALTV  48169  aacllem  49032