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  8100  omwordri  8499  omxpenlem  9006  infxpabs  10121  domfin4  10221  isf32lem7  10269  ordpipq  10853  muladd  11569  lemul12b  11998  mulge0b  12012  qaddcl  12878  iooshf  13342  elfzomelpfzo  13688  expnegz  14019  swrdccatin1  14648  bitsshft  16402  setscom  17107  lubun  18438  grplmulf1o  18943  grpraddf1o  18944  srhmsubc  20613  lmodfopne  20851  lidl1el  21181  frlmipval  21734  en2top  22929  cnpnei  23208  kgenidm  23491  ufileu  23863  fmfnfmlem4  23901  isngp4  24556  fsumcn  24817  evth  24914  cmslssbn  25328  mbfmulc2lem  25604  itg1addlem4  25656  dgreq0  26227  cxplt3  26665  cxple3  26666  basellem4  27050  ltssolem1  27643  nodenselem7  27658  zmulscld  28393  axcontlem2  29038  umgr2edg  29282  nbumgrvtx  29419  clwwlkf1  30124  umgrhashecclwwlk  30153  frgrncvvdeqlem9  30382  frgrwopreglem5ALT  30397  numclwwlk7lem  30464  grpoidinvlem3  30581  grpoideu  30584  grporcan  30593  3oalem2  31738  hmops  32095  adjadd  32168  mdslmd4i  32408  mdexchi  32410  mdsymlem1  32478  bnj607  35072  cvxsconn  35437  tailfb  36571  lindsadd  37814  poimirlem14  37835  mblfinlem4  37861  ismblfin  37862  ismtyres  38009  ghomco  38092  rngoisocnv  38182  1idl  38227  ps-2  39748  cfsetsnfsetf1  47315  usgrgrtrirex  48206  grlictr  48271  gpgvtx0  48309  srhmsubcALTV  48581  aacllem  50056