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  2786  ceqsrexbv  2935  euxfrdc  2990  eldifpr  3694  eldiftp  3713  eldifsn  3798  elrint  3966  elriin  4039  opeqsn  4343  rabxp  4761  eliunxp  4867  restidsing  5067  ressn  5275  fncnv  5393  dff1o5  5589  respreima  5771  dff4im  5789  dffo3  5790  f1ompt  5794  fsn  5815  fconst3m  5868  fconst4m  5869  eufnfv  5880  dff13  5904  f1mpt  5907  isores2  5949  isoini  5954  eloprabga  6103  mpomptx  6107  resoprab  6112  ov6g  6155  dfopab2  6347  dfoprab3s  6348  dfoprab3  6349  f1od2  6395  brtpos2  6412  dftpos3  6423  tpostpos  6425  dfsmo2  6448  elixp2  6866  mapsnen  6981  xpcomco  7005  eqinfti  7213  dfplpq2  7567  dfmpq2  7568  enq0enq  7644  nqnq0a  7667  nqnq0m  7668  genpassl  7737  genpassu  7738  axsuploc  8245  recexre  8751  recexgt0  8753  reapmul1  8768  apsqgt0  8774  apreim  8776  recexaplem2  8825  rerecclap  8903  elznn0  9487  elznn  9488  msqznn  9573  eluz2b1  9828  eluz2b3  9831  qreccl  9869  rpnegap  9914  elfz2nn0  10340  elfzo3  10392  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  qexpclz  10815  shftidt2  11386  clim0  11839  iser3shft  11900  summodclem3  11934  fprod2dlemstep  12176  eftlub  12244  ndvdsadd  12485  algfx  12617  isprm3  12683  isprm5  12707  xpsfrnel  13420  isabl2  13874  dvdsrcl2  14106  unitinvcl  14130  unitinvinv  14131  unitlinv  14133  unitrinv  14134  isrim  14176  isnzr2  14191  islmod  14298  isridl  14511  cnfldui  14596  ssntr  14839  tx1cn  14986  tx2cn  14987  pilem1  15496  lgsdir2lem4  15753