Theorem ad2ant2rl 736

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  omwordri  7991  omxpenlem  8406  infxpabs  9424  domfin4  9523  isf32lem7  9571  ordpipq  10154  muladd  10865  lemul12b  11290  mulge0b  11303  qaddcl  12172  iooshf  12624  elfzomelpfzo  12949  expnegz  13271  bitsshft  15674  setscom  16373  lubun  17581  grplmulf1o  17950  lmodfopne  19384  lidl1el  19702  frlmipval  20615  en2top  21287  cnpnei  21566  kgenidm  21849  ufileu  22221  fmfnfmlem4  22259  isngp4  22914  fsumcn  23171  evth  23256  cmslssbn  23668  mbfmulc2lem  23941  itg1addlem4  23993  dgreq0  24548  cxplt3  24974  cxple3  24975  basellem4  25353  axcontlem2  26444  umgr2edg  26684  nbumgrvtx  26821  clwwlkf1  27561  umgrhashecclwwlk  27592  frgrncvvdeqlem9  27831  frgrwopreglem5ALT  27846  numclwwlk7lem  27936  grpoidinvlem3  28050  grpoideu  28053  grporcan  28062  3oalem2  29211  hmops  29568  adjadd  29641  mdslmd4i  29881  mdexchi  29883  mdsymlem1  29951  bnj607  31796  cvxsconn  32035  poseq  32556  sltsolem1  32641  nodenselem7  32655  tailfb  33186  lindsadd  34274  poimirlem14  34295  mblfinlem4  34321  ismblfin  34322  ismtyres  34476  ghomco  34559  rngoisocnv  34649  1idl  34694  ps-2  36007  srhmsubc  43651  srhmsubcALTV  43669  aacllem  44209