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  4340  rabxp  4758  eliunxp  4864  restidsing  5064  ressn  5272  fncnv  5390  dff1o5  5586  respreima  5768  dff4im  5786  dffo3  5787  f1ompt  5791  fsn  5812  fconst3m  5865  fconst4m  5866  eufnfv  5877  dff13  5901  f1mpt  5904  isores2  5946  isoini  5951  eloprabga  6100  mpomptx  6104  resoprab  6109  ov6g  6152  dfopab2  6344  dfoprab3s  6345  dfoprab3  6346  f1od2  6392  brtpos2  6408  dftpos3  6419  tpostpos  6421  dfsmo2  6444  elixp2  6862  mapsnen  6977  xpcomco  6998  eqinfti  7203  dfplpq2  7557  dfmpq2  7558  enq0enq  7634  nqnq0a  7657  nqnq0m  7658  genpassl  7727  genpassu  7728  axsuploc  8235  recexre  8741  recexgt0  8743  reapmul1  8758  apsqgt0  8764  apreim  8766  recexaplem2  8815  rerecclap  8893  elznn0  9477  elznn  9478  msqznn  9563  eluz2b1  9813  eluz2b3  9816  qreccl  9854  rpnegap  9899  elfz2nn0  10325  elfzo3  10377  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  qexpclz  10799  shftidt2  11364  clim0  11817  iser3shft  11878  summodclem3  11912  fprod2dlemstep  12154  eftlub  12222  ndvdsadd  12463  algfx  12595  isprm3  12661  isprm5  12685  xpsfrnel  13398  isabl2  13852  dvdsrcl2  14084  unitinvcl  14108  unitinvinv  14109  unitlinv  14111  unitrinv  14112  isrim  14154  isnzr2  14169  islmod  14276  isridl  14489  cnfldui  14574  ssntr  14817  tx1cn  14964  tx2cn  14965  pilem1  15474  lgsdir2lem4  15731