Theorem pm5.32i 454

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 453	. 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  455  biadan2  456  anbi2i  457  abai  560  anabs5  573  pm5.33  609  eq2tri  2253  rexbiia  2509  reubiia  2679  rmobiia  2684  rabbiia  2745  ceqsrexbv  2892  euxfrdc  2947  eldifpr  3646  eldiftp  3665  eldifsn  3746  elrint  3911  elriin  3984  opeqsn  4282  rabxp  4697  eliunxp  4802  restidsing  4999  ressn  5207  fncnv  5321  dff1o5  5510  respreima  5687  dff4im  5705  dffo3  5706  f1ompt  5710  fsn  5731  fconst3m  5778  fconst4m  5779  eufnfv  5790  dff13  5812  f1mpt  5815  isores2  5857  isoini  5862  eloprabga  6006  mpomptx  6010  resoprab  6015  ov6g  6058  dfopab2  6244  dfoprab3s  6245  dfoprab3  6246  f1od2  6290  brtpos2  6306  dftpos3  6317  tpostpos  6319  dfsmo2  6342  elixp2  6758  mapsnen  6867  xpcomco  6882  eqinfti  7081  dfplpq2  7416  dfmpq2  7417  enq0enq  7493  nqnq0a  7516  nqnq0m  7517  genpassl  7586  genpassu  7587  axsuploc  8094  recexre  8599  recexgt0  8601  reapmul1  8616  apsqgt0  8622  apreim  8624  recexaplem2  8673  rerecclap  8751  elznn0  9335  elznn  9336  msqznn  9420  eluz2b1  9669  eluz2b3  9672  qreccl  9710  rpnegap  9755  elfz2nn0  10181  elfzo3  10233  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  qexpclz  10634  shftidt2  10979  clim0  11431  iser3shft  11492  summodclem3  11526  fprod2dlemstep  11768  eftlub  11836  ndvdsadd  12075  algfx  12193  isprm3  12259  isprm5  12283  xpsfrnel  12930  isabl2  13367  dvdsrcl2  13598  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  isrim  13668  isnzr2  13683  islmod  13790  isridl  14003  cnfldui  14088  ssntr  14301  tx1cn  14448  tx2cn  14449  pilem1  14955  lgsdir2lem4  15188