Theorem pm5.32i 450

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 449	. 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  451  biadan2  452  anbi2i  453  abai  550  anabs5  563  pm5.33  599  eq2tri  2214  rexbiia  2469  reubiia  2638  rmobiia  2643  rabbiia  2694  ceqsrexbv  2840  euxfrdc  2894  eldifpr  3583  eldiftp  3601  eldifsn  3682  elrint  3843  elriin  3915  opeqsn  4207  rabxp  4616  eliunxp  4718  ressn  5119  fncnv  5229  dff1o5  5416  respreima  5588  dff4im  5606  dffo3  5607  f1ompt  5611  fsn  5632  fconst3m  5679  fconst4m  5680  eufnfv  5688  dff13  5709  f1mpt  5712  isores2  5754  isoini  5759  eloprabga  5898  mpomptx  5902  resoprab  5907  ov6g  5948  dfopab2  6127  dfoprab3s  6128  dfoprab3  6129  f1od2  6172  brtpos2  6188  dftpos3  6199  tpostpos  6201  dfsmo2  6224  elixp2  6636  mapsnen  6745  xpcomco  6760  eqinfti  6952  dfplpq2  7253  dfmpq2  7254  enq0enq  7330  nqnq0a  7353  nqnq0m  7354  genpassl  7423  genpassu  7424  axsuploc  7929  recexre  8432  recexgt0  8434  reapmul1  8449  apsqgt0  8455  apreim  8457  recexaplem2  8505  rerecclap  8582  elznn0  9161  elznn  9162  msqznn  9243  eluz2b1  9490  eluz2b3  9493  qreccl  9529  rpnegap  9571  elfz2nn0  9992  elfzo3  10040  frecuzrdgtcl  10289  frecuzrdgfunlem  10296  qexpclz  10418  shftidt2  10709  clim0  11159  iser3shft  11220  summodclem3  11254  fprod2dlemstep  11496  eftlub  11564  ndvdsadd  11795  algfx  11900  isprm3  11966  ssntr  12461  tx1cn  12608  tx2cn  12609  pilem1  13039