Theorem dfifp2 1062

Description: Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒". This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1061). (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
dfifp2	⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))

Proof of Theorem dfifp2

Step	Hyp	Ref	Expression
1		df-ifp 1061	. 2 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))
2		cases2 1045	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
3	1, 2	bitri 274	1 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844  if-wif 1060

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 206  df-an 397  df-or 845  df-ifp 1061

This theorem is referenced by:  dfifp3  1063  dfifp5  1065  ifpdfbi  1068  ifpnOLD  1072  ifpimpda  1080  revwlk  33086  ifpbi2  41074  ifpbi3  41075  ifpbi23  41080  ifpbi1  41084  ifpbi12  41095  ifpbi13  41096  ifpimimb  41111  ifpororb  41112  ifpbibib  41117  frege54cor0a  41471