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  611  eq2tri  2289  rexbiia  2545  reubiia  2717  rmobiia  2722  rabbiia  2784  ceqsrexbv  2934  euxfrdc  2989  eldifpr  3693  eldiftp  3712  eldifsn  3795  elrint  3963  elriin  4036  opeqsn  4339  rabxp  4756  eliunxp  4861  restidsing  5061  ressn  5269  fncnv  5387  dff1o5  5583  respreima  5765  dff4im  5783  dffo3  5784  f1ompt  5788  fsn  5809  fconst3m  5862  fconst4m  5863  eufnfv  5874  dff13  5898  f1mpt  5901  isores2  5943  isoini  5948  eloprabga  6097  mpomptx  6101  resoprab  6106  ov6g  6149  dfopab2  6341  dfoprab3s  6342  dfoprab3  6343  f1od2  6387  brtpos2  6403  dftpos3  6414  tpostpos  6416  dfsmo2  6439  elixp2  6857  mapsnen  6972  xpcomco  6993  eqinfti  7195  dfplpq2  7549  dfmpq2  7550  enq0enq  7626  nqnq0a  7649  nqnq0m  7650  genpassl  7719  genpassu  7720  axsuploc  8227  recexre  8733  recexgt0  8735  reapmul1  8750  apsqgt0  8756  apreim  8758  recexaplem2  8807  rerecclap  8885  elznn0  9469  elznn  9470  msqznn  9555  eluz2b1  9804  eluz2b3  9807  qreccl  9845  rpnegap  9890  elfz2nn0  10316  elfzo3  10368  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  qexpclz  10790  shftidt2  11351  clim0  11804  iser3shft  11865  summodclem3  11899  fprod2dlemstep  12141  eftlub  12209  ndvdsadd  12450  algfx  12582  isprm3  12648  isprm5  12672  xpsfrnel  13385  isabl2  13839  dvdsrcl2  14071  unitinvcl  14095  unitinvinv  14096  unitlinv  14098  unitrinv  14099  isrim  14141  isnzr2  14156  islmod  14263  isridl  14476  cnfldui  14561  ssntr  14804  tx1cn  14951  tx2cn  14952  pilem1  15461  lgsdir2lem4  15718