Theorem pm5.32i 458

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32ri  459  biadan2  460  anbi2i  461  abai  566  anabs5  579  pm5.33  617  annotanannot  680  eq2tri  2298  rexbiia  2565  reubiia  2738  rmobiia  2743  rabbiia  2807  ceqsrexbv  2957  euxfrdc  3012  eldifpr  3735  eldiftp  3754  eldifsn  3839  elrint  4008  elriin  4081  opeqsn  4391  rabxp  4810  eliunxp  4917  restidsing  5117  ressn  5326  fncnv  5445  dff1o5  5646  respreima  5830  dff4im  5848  dffo3  5849  f1ompt  5853  fsn  5874  fconst3m  5928  fconst4m  5929  eufnfv  5943  dff13  5968  f1mpt  5971  isores2  6013  isoini  6018  eloprabga  6169  mpomptx  6173  resoprab  6178  ov6g  6221  dfopab2  6417  dfoprab3s  6418  dfoprab3  6419  f1od2  6465  brtpos2  6516  dftpos3  6527  tpostpos  6529  dfsmo2  6552  elixp2  6978  mapsnen  7094  xpcomco  7118  eqinfti  7354  dfplpq2  7715  dfmpq2  7716  enq0enq  7792  nqnq0a  7815  nqnq0m  7816  genpassl  7885  genpassu  7886  axsuploc  8392  recexre  8900  recexgt0  8902  reapmul1  8917  apsqgt0  8923  apreim  8925  recexaplem2  8974  rerecclap  9054  elznn0  9642  elznn  9643  msqznn  9729  eluz2b1  9984  eluz2b3  9987  qreccl  10025  rpnegap  10070  elfz2nn0  10502  elfzo3  10554  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  qexpclz  10980  shftidt2  11580  clim0  12034  iser3shft  12095  summodclem3  12130  fprod2dlemstep  12372  eftlub  12440  ndvdsadd  12681  algfx  12813  isprm3  12879  isprm5  12903  ballotfilemodife  13223  xpsfrnel  13648  isabl2  14080  dvdsrcl2  14389  unitinvcl  14413  unitinvinv  14414  unitlinv  14416  unitrinv  14417  isrim  14459  isnzr2  14474  drngprop  14600  islmod  14610  isridl  14824  cnfldui  14907  isassa  14985  ssntr  15206  tx1cn  15353  tx2cn  15354  pilem1  15863  lgsdir2lem4  16133  alsralrex  17127  dfalseu2  17151