Theorem ad2ant2rl 750

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 716	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  8108  omwordri  8507  omxpenlem  9016  infxpabs  10133  domfin4  10233  isf32lem7  10281  ordpipq  10865  muladd  11582  lemul12b  12012  mulge0b  12026  qaddcl  12915  iooshf  13379  elfzomelpfzo  13727  expnegz  14058  swrdccatin1  14687  bitsshft  16444  setscom  17150  lubun  18481  grplmulf1o  18989  grpraddf1o  18990  srhmsubc  20657  lmodfopne  20895  lidl1el  21224  frlmipval  21759  en2top  22950  cnpnei  23229  kgenidm  23512  ufileu  23884  fmfnfmlem4  23922  isngp4  24577  fsumcn  24837  evth  24926  cmslssbn  25339  mbfmulc2lem  25614  itg1addlem4  25666  dgreq0  26230  cxplt3  26664  cxple3  26665  basellem4  27047  ltssolem1  27639  nodenselem7  27654  zmulscld  28389  axcontlem2  29034  umgr2edg  29278  nbumgrvtx  29415  clwwlkf1  30119  umgrhashecclwwlk  30148  frgrncvvdeqlem9  30377  frgrwopreglem5ALT  30392  numclwwlk7lem  30459  grpoidinvlem3  30577  grpoideu  30580  grporcan  30589  3oalem2  31734  hmops  32091  adjadd  32164  mdslmd4i  32404  mdexchi  32406  mdsymlem1  32474  bnj607  35058  cvxsconn  35425  tailfb  36559  lindsadd  37934  poimirlem14  37955  mblfinlem4  37981  ismblfin  37982  ismtyres  38129  ghomco  38212  rngoisocnv  38302  1idl  38347  ps-2  39924  cfsetsnfsetf1  47507  usgrgrtrirex  48426  grlictr  48491  gpgvtx0  48529  srhmsubcALTV  48801  aacllem  50276