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 399

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 210  df-an 400

This theorem is referenced by:  omwordri  8181  omxpenlem  8601  infxpabs  9623  domfin4  9722  isf32lem7  9770  ordpipq  10353  muladd  11061  lemul12b  11486  mulge0b  11499  qaddcl  12352  iooshf  12804  elfzomelpfzo  13136  expnegz  13459  swrdccatin1  14078  bitsshft  15814  setscom  16519  lubun  17725  grplmulf1o  18165  lmodfopne  19665  lidl1el  19984  frlmipval  20468  en2top  21590  cnpnei  21869  kgenidm  22152  ufileu  22524  fmfnfmlem4  22562  isngp4  23218  fsumcn  23475  evth  23564  cmslssbn  23976  mbfmulc2lem  24251  itg1addlem4  24303  dgreq0  24862  cxplt3  25291  cxple3  25292  basellem4  25669  axcontlem2  26759  umgr2edg  26999  nbumgrvtx  27136  clwwlkf1  27834  umgrhashecclwwlk  27863  frgrncvvdeqlem9  28092  frgrwopreglem5ALT  28107  numclwwlk7lem  28174  grpoidinvlem3  28289  grpoideu  28292  grporcan  28301  3oalem2  29446  hmops  29803  adjadd  29876  mdslmd4i  30116  mdexchi  30118  mdsymlem1  30186  bnj607  32298  cvxsconn  32603  poseq  33208  sltsolem1  33293  nodenselem7  33307  tailfb  33838  lindsadd  35050  poimirlem14  35071  mblfinlem4  35097  ismblfin  35098  ismtyres  35246  ghomco  35329  rngoisocnv  35419  1idl  35464  ps-2  36774  srhmsubc  44700  srhmsubcALTV  44718  aacllem  45329