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  8114  omwordri  8513  omxpenlem  9019  infxpabs  10140  domfin4  10240  isf32lem7  10288  ordpipq  10871  muladd  11586  lemul12b  12015  mulge0b  12029  qaddcl  12900  iooshf  13363  elfzomelpfzo  13708  expnegz  14037  swrdccatin1  14666  bitsshft  16421  setscom  17126  lubun  18456  grplmulf1o  18927  grpraddf1o  18928  srhmsubc  20600  lmodfopne  20838  lidl1el  21168  frlmipval  21721  en2top  22905  cnpnei  23184  kgenidm  23467  ufileu  23839  fmfnfmlem4  23877  isngp4  24533  fsumcn  24794  evth  24891  cmslssbn  25305  mbfmulc2lem  25581  itg1addlem4  25633  dgreq0  26204  cxplt3  26642  cxple3  26643  basellem4  27027  sltsolem1  27620  nodenselem7  27635  zmulscld  28325  axcontlem2  28945  umgr2edg  29189  nbumgrvtx  29326  clwwlkf1  30028  umgrhashecclwwlk  30057  frgrncvvdeqlem9  30286  frgrwopreglem5ALT  30301  numclwwlk7lem  30368  grpoidinvlem3  30485  grpoideu  30488  grporcan  30497  3oalem2  31642  hmops  31999  adjadd  32072  mdslmd4i  32312  mdexchi  32314  mdsymlem1  32382  bnj607  34899  cvxsconn  35223  tailfb  36358  lindsadd  37600  poimirlem14  37621  mblfinlem4  37647  ismblfin  37648  ismtyres  37795  ghomco  37878  rngoisocnv  37968  1idl  38013  ps-2  39465  cfsetsnfsetf1  47053  usgrgrtrirex  47942  grlictr  48000  gpgvtx0  48037  srhmsubcALTV  48306  aacllem  49783