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  562  anabs5  575  pm5.33  613  annotanannot  676  eq2tri  2292  rexbiia  2557  reubiia  2729  rmobiia  2734  rabbiia  2798  ceqsrexbv  2947  euxfrdc  3002  eldifpr  3715  eldiftp  3734  eldifsn  3819  elrint  3988  elriin  4061  opeqsn  4368  rabxp  4786  eliunxp  4893  restidsing  5093  ressn  5302  fncnv  5421  dff1o5  5622  respreima  5804  dff4im  5822  dffo3  5823  f1ompt  5827  fsn  5848  fconst3m  5902  fconst4m  5903  eufnfv  5916  dff13  5940  f1mpt  5943  isores2  5985  isoini  5990  eloprabga  6139  mpomptx  6143  resoprab  6148  ov6g  6191  dfopab2  6382  dfoprab3s  6383  dfoprab3  6384  f1od2  6430  brtpos2  6481  dftpos3  6492  tpostpos  6494  dfsmo2  6517  elixp2  6936  mapsnen  7052  xpcomco  7076  eqinfti  7310  dfplpq2  7668  dfmpq2  7669  enq0enq  7745  nqnq0a  7768  nqnq0m  7769  genpassl  7838  genpassu  7839  axsuploc  8345  recexre  8851  recexgt0  8853  reapmul1  8868  apsqgt0  8874  apreim  8876  recexaplem2  8925  rerecclap  9003  elznn0  9591  elznn  9592  msqznn  9677  eluz2b1  9932  eluz2b3  9935  qreccl  9973  rpnegap  10018  elfz2nn0  10445  elfzo3  10497  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  qexpclz  10921  shftidt2  11513  clim0  11966  iser3shft  12027  summodclem3  12062  fprod2dlemstep  12304  eftlub  12372  ndvdsadd  12613  algfx  12745  isprm3  12811  isprm5  12835  xpsfrnel  13549  isabl2  14003  dvdsrcl2  14236  unitinvcl  14260  unitinvinv  14261  unitlinv  14263  unitrinv  14264  isrim  14306  isnzr2  14321  islmod  14431  isridl  14644  cnfldui  14729  ssntr  14979  tx1cn  15126  tx2cn  15127  pilem1  15636  lgsdir2lem4  15896