Theorem pm5.32i 449

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

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 448	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 144	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32ri  450  biadan2  451  anbi2i  452  abai  549  anabs5  562  pm5.33  598  eq2tri  2199  rexbiia  2450  reubiia  2615  rmobiia  2620  rabbiia  2671  ceqsrexbv  2816  euxfrdc  2870  eldifsn  3650  elrint  3811  elriin  3883  opeqsn  4174  rabxp  4576  eliunxp  4678  ressn  5079  fncnv  5189  dff1o5  5376  respreima  5548  dff4im  5566  dffo3  5567  f1ompt  5571  fsn  5592  fconst3m  5639  fconst4m  5640  eufnfv  5648  dff13  5669  f1mpt  5672  isores2  5714  isoini  5719  eloprabga  5858  mpomptx  5862  resoprab  5867  ov6g  5908  dfopab2  6087  dfoprab3s  6088  dfoprab3  6089  f1od2  6132  brtpos2  6148  dftpos3  6159  tpostpos  6161  dfsmo2  6184  elixp2  6596  mapsnen  6705  xpcomco  6720  eqinfti  6907  dfplpq2  7162  dfmpq2  7163  enq0enq  7239  nqnq0a  7262  nqnq0m  7263  genpassl  7332  genpassu  7333  axsuploc  7837  recexre  8340  recexgt0  8342  reapmul1  8357  apsqgt0  8363  apreim  8365  recexaplem2  8413  rerecclap  8490  elznn0  9069  elznn  9070  msqznn  9151  eluz2b1  9395  eluz2b3  9398  qreccl  9434  rpnegap  9474  elfz2nn0  9892  elfzo3  9940  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  qexpclz  10314  shftidt2  10604  clim0  11054  iser3shft  11115  summodclem3  11149  eftlub  11396  ndvdsadd  11628  algfx  11733  isprm3  11799  ssntr  12291  tx1cn  12438  tx2cn  12439  pilem1  12860