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  8088  omwordri  8487  omxpenlem  8991  infxpabs  10102  domfin4  10202  isf32lem7  10250  ordpipq  10833  muladd  11549  lemul12b  11978  mulge0b  11992  qaddcl  12863  iooshf  13326  elfzomelpfzo  13672  expnegz  14003  swrdccatin1  14632  bitsshft  16386  setscom  17091  lubun  18421  grplmulf1o  18926  grpraddf1o  18927  srhmsubc  20595  lmodfopne  20833  lidl1el  21163  frlmipval  21716  en2top  22900  cnpnei  23179  kgenidm  23462  ufileu  23834  fmfnfmlem4  23872  isngp4  24527  fsumcn  24788  evth  24885  cmslssbn  25299  mbfmulc2lem  25575  itg1addlem4  25627  dgreq0  26198  cxplt3  26636  cxple3  26637  basellem4  27021  sltsolem1  27614  nodenselem7  27629  zmulscld  28321  axcontlem2  28943  umgr2edg  29187  nbumgrvtx  29324  clwwlkf1  30029  umgrhashecclwwlk  30058  frgrncvvdeqlem9  30287  frgrwopreglem5ALT  30302  numclwwlk7lem  30369  grpoidinvlem3  30486  grpoideu  30489  grporcan  30498  3oalem2  31643  hmops  32000  adjadd  32073  mdslmd4i  32313  mdexchi  32315  mdsymlem1  32383  bnj607  34928  cvxsconn  35287  tailfb  36421  lindsadd  37663  poimirlem14  37684  mblfinlem4  37710  ismblfin  37711  ismtyres  37858  ghomco  37941  rngoisocnv  38031  1idl  38076  ps-2  39587  cfsetsnfsetf1  47169  usgrgrtrirex  48060  grlictr  48125  gpgvtx0  48163  srhmsubcALTV  48435  aacllem  49912