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  2226  rexbiia  2481  reubiia  2650  rmobiia  2655  rabbiia  2711  ceqsrexbv  2857  euxfrdc  2912  eldifpr  3603  eldiftp  3622  eldifsn  3703  elrint  3864  elriin  3936  opeqsn  4230  rabxp  4641  eliunxp  4743  ressn  5144  fncnv  5254  dff1o5  5441  respreima  5613  dff4im  5631  dffo3  5632  f1ompt  5636  fsn  5657  fconst3m  5704  fconst4m  5705  eufnfv  5715  dff13  5736  f1mpt  5739  isores2  5781  isoini  5786  eloprabga  5929  mpomptx  5933  resoprab  5938  ov6g  5979  dfopab2  6157  dfoprab3s  6158  dfoprab3  6159  f1od2  6203  brtpos2  6219  dftpos3  6230  tpostpos  6232  dfsmo2  6255  elixp2  6668  mapsnen  6777  xpcomco  6792  eqinfti  6985  dfplpq2  7295  dfmpq2  7296  enq0enq  7372  nqnq0a  7395  nqnq0m  7396  genpassl  7465  genpassu  7466  axsuploc  7971  recexre  8476  recexgt0  8478  reapmul1  8493  apsqgt0  8499  apreim  8501  recexaplem2  8549  rerecclap  8626  elznn0  9206  elznn  9207  msqznn  9291  eluz2b1  9539  eluz2b3  9542  qreccl  9580  rpnegap  9622  elfz2nn0  10047  elfzo3  10098  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  qexpclz  10476  shftidt2  10774  clim0  11226  iser3shft  11287  summodclem3  11321  fprod2dlemstep  11563  eftlub  11631  ndvdsadd  11868  algfx  11984  isprm3  12050  isprm5  12074  ssntr  12762  tx1cn  12909  tx2cn  12910  pilem1  13340  lgsdir2lem4  13572