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  2291  rexbiia  2548  reubiia  2720  rmobiia  2725  rabbiia  2789  ceqsrexbv  2938  euxfrdc  2993  eldifpr  3700  eldiftp  3719  eldifsn  3804  elrint  3973  elriin  4046  opeqsn  4351  rabxp  4769  eliunxp  4875  restidsing  5075  ressn  5284  fncnv  5403  dff1o5  5601  respreima  5783  dff4im  5801  dffo3  5802  f1ompt  5806  fsn  5827  fconst3m  5881  fconst4m  5882  eufnfv  5895  dff13  5919  f1mpt  5922  isores2  5964  isoini  5969  eloprabga  6118  mpomptx  6122  resoprab  6127  ov6g  6170  dfopab2  6361  dfoprab3s  6362  dfoprab3  6363  f1od2  6409  brtpos2  6460  dftpos3  6471  tpostpos  6473  dfsmo2  6496  elixp2  6914  mapsnen  7029  xpcomco  7053  eqinfti  7262  dfplpq2  7617  dfmpq2  7618  enq0enq  7694  nqnq0a  7717  nqnq0m  7718  genpassl  7787  genpassu  7788  axsuploc  8295  recexre  8801  recexgt0  8803  reapmul1  8818  apsqgt0  8824  apreim  8826  recexaplem2  8875  rerecclap  8953  elznn0  9537  elznn  9538  msqznn  9623  eluz2b1  9878  eluz2b3  9881  qreccl  9919  rpnegap  9964  elfz2nn0  10390  elfzo3  10442  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  qexpclz  10866  shftidt2  11453  clim0  11906  iser3shft  11967  summodclem3  12002  fprod2dlemstep  12244  eftlub  12312  ndvdsadd  12553  algfx  12685  isprm3  12751  isprm5  12775  xpsfrnel  13488  isabl2  13942  dvdsrcl2  14175  unitinvcl  14199  unitinvinv  14200  unitlinv  14202  unitrinv  14203  isrim  14245  isnzr2  14260  islmod  14367  isridl  14580  cnfldui  14665  ssntr  14913  tx1cn  15060  tx2cn  15061  pilem1  15570  lgsdir2lem4  15830