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  2266  rexbiia  2522  reubiia  2692  rmobiia  2697  rabbiia  2758  ceqsrexbv  2906  euxfrdc  2961  eldifpr  3662  eldiftp  3681  eldifsn  3763  elrint  3928  elriin  4001  opeqsn  4302  rabxp  4717  eliunxp  4822  restidsing  5021  ressn  5229  fncnv  5346  dff1o5  5540  respreima  5718  dff4im  5736  dffo3  5737  f1ompt  5741  fsn  5762  fconst3m  5813  fconst4m  5814  eufnfv  5825  dff13  5847  f1mpt  5850  isores2  5892  isoini  5897  eloprabga  6042  mpomptx  6046  resoprab  6051  ov6g  6094  dfopab2  6285  dfoprab3s  6286  dfoprab3  6287  f1od2  6331  brtpos2  6347  dftpos3  6358  tpostpos  6360  dfsmo2  6383  elixp2  6799  mapsnen  6914  xpcomco  6933  eqinfti  7134  dfplpq2  7480  dfmpq2  7481  enq0enq  7557  nqnq0a  7580  nqnq0m  7581  genpassl  7650  genpassu  7651  axsuploc  8158  recexre  8664  recexgt0  8666  reapmul1  8681  apsqgt0  8687  apreim  8689  recexaplem2  8738  rerecclap  8816  elznn0  9400  elznn  9401  msqznn  9486  eluz2b1  9735  eluz2b3  9738  qreccl  9776  rpnegap  9821  elfz2nn0  10247  elfzo3  10299  frecuzrdgtcl  10570  frecuzrdgfunlem  10577  qexpclz  10718  shftidt2  11193  clim0  11646  iser3shft  11707  summodclem3  11741  fprod2dlemstep  11983  eftlub  12051  ndvdsadd  12292  algfx  12424  isprm3  12490  isprm5  12514  xpsfrnel  13226  isabl2  13680  dvdsrcl2  13911  unitinvcl  13935  unitinvinv  13936  unitlinv  13938  unitrinv  13939  isrim  13981  isnzr2  13996  islmod  14103  isridl  14316  cnfldui  14401  ssntr  14644  tx1cn  14791  tx2cn  14792  pilem1  15301  lgsdir2lem4  15558