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 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

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:  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  3736  eldiftp  3755  eldifsn  3841  elrint  4010  elriin  4083  opeqsn  4393  rabxp  4812  eliunxp  4919  restidsing  5119  ressn  5328  fncnv  5447  dff1o5  5648  respreima  5836  dff4im  5854  dffo3  5855  f1ompt  5859  fsn  5880  fconst3m  5934  fconst4m  5935  eufnfv  5949  dff13  5974  f1mpt  5977  isores2  6019  isoini  6024  eloprabga  6175  mpomptx  6179  resoprab  6184  ov6g  6227  dfopab2  6423  dfoprab3s  6424  dfoprab3  6425  f1od2  6471  brtpos2  6522  dftpos3  6533  tpostpos  6535  dfsmo2  6558  elixp2  6984  mapsnen  7100  xpcomco  7124  eqinfti  7360  dfplpq2  7721  dfmpq2  7722  enq0enq  7798  nqnq0a  7821  nqnq0m  7822  genpassl  7891  genpassu  7892  axsuploc  8398  recexre  8907  recexgt0  8909  reapmul1  8924  apsqgt0  8930  apreim  8932  recexaplem2  8981  rerecclap  9061  elznn0  9661  elznn  9662  msqznn  9748  eluz2b1  10003  eluz2b3  10006  qreccl  10044  rpnegap  10089  elfz2nn0  10521  elfzo3  10573  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  qexpclz  10999  shftidt2  11599  clim0  12053  iser3shft  12114  summodclem3  12149  fprod2dlemstep  12391  eftlub  12459  ndvdsadd  12700  algfx  12832  isprm3  12898  isprm5  12922  ballotfilemodife  13242  xpsfrnel  13667  isabl2  14099  dvdsrcl2  14408  unitinvcl  14432  unitinvinv  14433  unitlinv  14435  unitrinv  14436  isrim  14478  isnzr2  14493  drngprop  14619  islmod  14629  isridl  14843  cnfldui  14926  isassa  15004  ssntr  15225  tx1cn  15372  tx2cn  15373  pilem1  15883  lgsdir2lem4  16162  alsralrex  17165  dfalseu2  17189