Theorem pm5.32i 489

Description: Distribution of implication over biconditional (inference rule).

Hypothesis

Ref	Expression
pm5.32i.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
pm5.32i	⊢ ((φ ∧ ψ) ↔ (φ ∧ χ))

Proof of Theorem pm5.32i

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		pm5.32 488	. 2 ⊢ ((φ → (ψ ↔ χ)) ↔ ((φ ∧ ψ) ↔ (φ ∧ χ)))
3	1, 2	mpbi 164	1 ⊢ ((φ ∧ ψ) ↔ (φ ∧ χ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  pm5.32ri 490  cleq2tr 1148  birexa 1229  bireua 1319  birabi 1342  gencbvex 1372  euxfr 1436  elrabsf 1456  reuxfr 1580  dflim2 2280  onzsl 2367  dfom2 2374  cbvop 2473  relss 2480  iss 2599  fsn 2895  f1fv 2916  isoini 2938  tz7.48-1 2994  eloprabg 3035  fnoprval 3042  mapsnen 3334  aceq5lem1 3558  iscard 3659  iscard2 3660  cardval2 3661  isinfcard 3692  elni2 3799  indpi 3828  genpass 3906  reclem1pr 3950  elreal 4044  sup3 4511  elnn0z 4574  elznn0 4576  elnn0nn 4593  elnnnn0 4594  seqlem2 4663  ruclem13 4897  dfchsup2 5299  dfchj2 5325  dfchj3 5326  h1det 5455  elat2 5739

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org