Theorem ad2ant2rl 745

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 712	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 711	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 206  df-an 396

This theorem is referenced by:  omwordri  8365  omxpenlem  8813  infxpabs  9899  domfin4  9998  isf32lem7  10046  ordpipq  10629  muladd  11337  lemul12b  11762  mulge0b  11775  qaddcl  12634  iooshf  13087  elfzomelpfzo  13419  expnegz  13745  swrdccatin1  14366  bitsshft  16110  setscom  16809  lubun  18148  grplmulf1o  18564  lmodfopne  20076  lidl1el  20402  frlmipval  20896  en2top  22043  cnpnei  22323  kgenidm  22606  ufileu  22978  fmfnfmlem4  23016  isngp4  23674  fsumcn  23939  evth  24028  cmslssbn  24441  mbfmulc2lem  24716  itg1addlem4  24768  itg1addlem4OLD  24769  dgreq0  25331  cxplt3  25760  cxple3  25761  basellem4  26138  axcontlem2  27236  umgr2edg  27479  nbumgrvtx  27616  clwwlkf1  28314  umgrhashecclwwlk  28343  frgrncvvdeqlem9  28572  frgrwopreglem5ALT  28587  numclwwlk7lem  28654  grpoidinvlem3  28769  grpoideu  28772  grporcan  28781  3oalem2  29926  hmops  30283  adjadd  30356  mdslmd4i  30596  mdexchi  30598  mdsymlem1  30666  bnj607  32796  cvxsconn  33105  poseq  33729  sltsolem1  33805  nodenselem7  33820  tailfb  34493  lindsadd  35697  poimirlem14  35718  mblfinlem4  35744  ismblfin  35745  ismtyres  35893  ghomco  35976  rngoisocnv  36066  1idl  36111  ps-2  37419  cfsetsnfsetf1  44440  srhmsubc  45522  srhmsubcALTV  45540  aacllem  46391