Theorem iba 300

Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) (Revised by NM, 24-Mar-2013.)

Assertion

Ref	Expression
iba	⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		pm3.21 264	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 142	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantru  302  biantrud  304  ancrb  322  rbaibd  936  dedlem0a  981  fvopab6  5808  fressnfv  5905  tpostpos  6540  nnmword  6796  unfiexmid  7231  ltmpig  7712  mul0eqap  9008  sup3exmid  9295  xrmaxiflemcom  12039  rexrals  17374  rexals  17380