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  eq2tri  2291  rexbiia  2547  reubiia  2719  rmobiia  2724  rabbiia  2788  ceqsrexbv  2937  euxfrdc  2992  eldifpr  3696  eldiftp  3715  eldifsn  3800  elrint  3968  elriin  4041  opeqsn  4345  rabxp  4763  eliunxp  4869  restidsing  5069  ressn  5277  fncnv  5396  dff1o5  5592  respreima  5775  dff4im  5793  dffo3  5794  f1ompt  5798  fsn  5819  fconst3m  5873  fconst4m  5874  eufnfv  5885  dff13  5909  f1mpt  5912  isores2  5954  isoini  5959  eloprabga  6108  mpomptx  6112  resoprab  6117  ov6g  6160  dfopab2  6352  dfoprab3s  6353  dfoprab3  6354  f1od2  6400  brtpos2  6417  dftpos3  6428  tpostpos  6430  dfsmo2  6453  elixp2  6871  mapsnen  6986  xpcomco  7010  eqinfti  7219  dfplpq2  7574  dfmpq2  7575  enq0enq  7651  nqnq0a  7674  nqnq0m  7675  genpassl  7744  genpassu  7745  axsuploc  8252  recexre  8758  recexgt0  8760  reapmul1  8775  apsqgt0  8781  apreim  8783  recexaplem2  8832  rerecclap  8910  elznn0  9494  elznn  9495  msqznn  9580  eluz2b1  9835  eluz2b3  9838  qreccl  9876  rpnegap  9921  elfz2nn0  10347  elfzo3  10399  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  qexpclz  10823  shftidt2  11397  clim0  11850  iser3shft  11911  summodclem3  11946  fprod2dlemstep  12188  eftlub  12256  ndvdsadd  12497  algfx  12629  isprm3  12695  isprm5  12719  xpsfrnel  13432  isabl2  13886  dvdsrcl2  14119  unitinvcl  14143  unitinvinv  14144  unitlinv  14146  unitrinv  14147  isrim  14189  isnzr2  14204  islmod  14311  isridl  14524  cnfldui  14609  ssntr  14852  tx1cn  14999  tx2cn  15000  pilem1  15509  lgsdir2lem4  15766