Theorem ad2ant2rl 748

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 715	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 714	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  8199  omwordri  8628  omxpenlem  9139  infxpabs  10280  domfin4  10380  isf32lem7  10428  ordpipq  11011  muladd  11722  lemul12b  12151  mulge0b  12165  qaddcl  13030  iooshf  13486  elfzomelpfzo  13821  expnegz  14147  swrdccatin1  14773  bitsshft  16521  setscom  17227  lubun  18585  grplmulf1o  19053  grpraddf1o  19054  srhmsubc  20702  lmodfopne  20920  lidl1el  21259  frlmipval  21822  en2top  23013  cnpnei  23293  kgenidm  23576  ufileu  23948  fmfnfmlem4  23986  isngp4  24646  fsumcn  24913  evth  25010  cmslssbn  25425  mbfmulc2lem  25701  itg1addlem4  25753  itg1addlem4OLD  25754  dgreq0  26325  cxplt3  26760  cxple3  26761  basellem4  27145  sltsolem1  27738  nodenselem7  27753  zmulscld  28401  axcontlem2  28998  umgr2edg  29244  nbumgrvtx  29381  clwwlkf1  30081  umgrhashecclwwlk  30110  frgrncvvdeqlem9  30339  frgrwopreglem5ALT  30354  numclwwlk7lem  30421  grpoidinvlem3  30538  grpoideu  30541  grporcan  30550  3oalem2  31695  hmops  32052  adjadd  32125  mdslmd4i  32365  mdexchi  32367  mdsymlem1  32435  bnj607  34892  cvxsconn  35211  tailfb  36343  lindsadd  37573  poimirlem14  37594  mblfinlem4  37620  ismblfin  37621  ismtyres  37768  ghomco  37851  rngoisocnv  37941  1idl  37986  ps-2  39435  cfsetsnfsetf1  46974  usgrgrtrirex  47799  grlictr  47832  srhmsubcALTV  48048  aacllem  48895