Theorem 3anidm12 1422

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

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

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 1089

This theorem is referenced by:  3anidm13  1423  syl2an3an  1425  dedth3v  4531  fovcl  7490  nncan  11418  divid  11835  dividOLD  11836  sqdivid  14079  subsq  14167  o1lo1  15494  retancl  16104  tanneg  16110  gcd0id  16483  coprm  16676  ablonncan  30646  kbpj  32046  xdivid  33006  xrsmulgzz  33088  f1resrcmplf1dlem  35249  expgrowthi  44784  dvconstbi  44785  3ornot23  44960  3anidm12p2  45257  sinhpcosh  50233  reseccl  50246  recsccl  50247  recotcl  50248  onetansqsecsq  50254