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  8157  omwordri  8584  omxpenlem  9087  infxpabs  10225  domfin4  10325  isf32lem7  10373  ordpipq  10956  muladd  11669  lemul12b  12098  mulge0b  12112  qaddcl  12981  iooshf  13443  elfzomelpfzo  13787  expnegz  14114  swrdccatin1  14743  bitsshft  16494  setscom  17199  lubun  18525  grplmulf1o  18996  grpraddf1o  18997  srhmsubc  20640  lmodfopne  20857  lidl1el  21187  frlmipval  21739  en2top  22923  cnpnei  23202  kgenidm  23485  ufileu  23857  fmfnfmlem4  23895  isngp4  24551  fsumcn  24812  evth  24909  cmslssbn  25324  mbfmulc2lem  25600  itg1addlem4  25652  dgreq0  26223  cxplt3  26661  cxple3  26662  basellem4  27046  sltsolem1  27639  nodenselem7  27654  zmulscld  28337  axcontlem2  28944  umgr2edg  29188  nbumgrvtx  29325  clwwlkf1  30030  umgrhashecclwwlk  30059  frgrncvvdeqlem9  30288  frgrwopreglem5ALT  30303  numclwwlk7lem  30370  grpoidinvlem3  30487  grpoideu  30490  grporcan  30499  3oalem2  31644  hmops  32001  adjadd  32074  mdslmd4i  32314  mdexchi  32316  mdsymlem1  32384  bnj607  34947  cvxsconn  35265  tailfb  36395  lindsadd  37637  poimirlem14  37658  mblfinlem4  37684  ismblfin  37685  ismtyres  37832  ghomco  37915  rngoisocnv  38005  1idl  38050  ps-2  39497  cfsetsnfsetf1  47088  usgrgrtrirex  47962  grlictr  48020  gpgvtx0  48057  srhmsubcALTV  48300  aacllem  49665