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  5805  fressnfv  5902  tpostpos  6535  nnmword  6791  unfiexmid  7225  ltmpig  7706  mul0eqap  9000  sup3exmid  9287  xrmaxiflemcom  12015  rexrals  17150  rexals  17156