Theorem 3anidm12 1421

Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)

Hypothesis

Ref	Expression
3anidm12.1	⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3anidm12	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3anidm12

Step	Hyp	Ref	Expression
1		3anidm12.1	. . 3 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)
2	1	3expib 1122	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	2	anabsi5 669	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3anidm13  1422  syl2an3an  1424  dedth3v  4569  fovcl  7540  nncan  11517  divid  11932  dividOLD  11933  sqdivid  14145  subsq  14233  o1lo1  15558  retancl  16165  tanneg  16171  gcd0id  16543  coprm  16735  ablonncan  30542  kbpj  31942  xdivid  32907  xrsmulgzz  33006  f1resrcmplf1dlem  35122  expgrowthi  44324  dvconstbi  44325  3ornot23  44501  3anidm12p2  44798  sinhpcosh  49571  reseccl  49584  recsccl  49585  recotcl  49586  onetansqsecsq  49592