Theorem ad2ant2rl 747

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  omwordri  8198  omxpenlem  8618  infxpabs  9634  domfin4  9733  isf32lem7  9781  ordpipq  10364  muladd  11072  lemul12b  11497  mulge0b  11510  qaddcl  12365  iooshf  12816  elfzomelpfzo  13142  expnegz  13464  swrdccatin1  14087  bitsshft  15824  setscom  16527  lubun  17733  grplmulf1o  18173  lmodfopne  19672  lidl1el  19991  frlmipval  20923  en2top  21593  cnpnei  21872  kgenidm  22155  ufileu  22527  fmfnfmlem4  22565  isngp4  23221  fsumcn  23478  evth  23563  cmslssbn  23975  mbfmulc2lem  24248  itg1addlem4  24300  dgreq0  24855  cxplt3  25283  cxple3  25284  basellem4  25661  axcontlem2  26751  umgr2edg  26991  nbumgrvtx  27128  clwwlkf1  27828  umgrhashecclwwlk  27857  frgrncvvdeqlem9  28086  frgrwopreglem5ALT  28101  numclwwlk7lem  28168  grpoidinvlem3  28283  grpoideu  28286  grporcan  28295  3oalem2  29440  hmops  29797  adjadd  29870  mdslmd4i  30110  mdexchi  30112  mdsymlem1  30180  bnj607  32188  cvxsconn  32490  poseq  33095  sltsolem1  33180  nodenselem7  33194  tailfb  33725  lindsadd  34900  poimirlem14  34921  mblfinlem4  34947  ismblfin  34948  ismtyres  35101  ghomco  35184  rngoisocnv  35274  1idl  35319  ps-2  36629  srhmsubc  44367  srhmsubcALTV  44385  aacllem  44922