Theorem 3anidm12 1546

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 1156	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))
3	2	anabsi5 659	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111

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 387  df-3an 1113

This theorem is referenced by:  3anidm13  1547  syl2an3an  1549  dedth3v  4369  nncan  10638  divid  11046  sqdivid  13230  subsq  13273  o1lo1  14652  retancl  15251  tanneg  15257  gcd0id  15620  coprm  15801  ablonncan  27962  kbpj  29366  xdivid  30177  xrsmulgzz  30219  expgrowthi  39367  dvconstbi  39368  3ornot23  39548  3anidm12p2  39856  sinhpcosh  43389  reseccl  43402  recsccl  43403  recotcl  43404  onetansqsecsq  43410