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  2256  rexbiia  2512  reubiia  2682  rmobiia  2687  rabbiia  2748  ceqsrexbv  2895  euxfrdc  2950  eldifpr  3650  eldiftp  3669  eldifsn  3750  elrint  3915  elriin  3988  opeqsn  4286  rabxp  4701  eliunxp  4806  restidsing  5003  ressn  5211  fncnv  5325  dff1o5  5516  respreima  5693  dff4im  5711  dffo3  5712  f1ompt  5716  fsn  5737  fconst3m  5784  fconst4m  5785  eufnfv  5796  dff13  5818  f1mpt  5821  isores2  5863  isoini  5868  eloprabga  6013  mpomptx  6017  resoprab  6022  ov6g  6065  dfopab2  6256  dfoprab3s  6257  dfoprab3  6258  f1od2  6302  brtpos2  6318  dftpos3  6329  tpostpos  6331  dfsmo2  6354  elixp2  6770  mapsnen  6879  xpcomco  6894  eqinfti  7095  dfplpq2  7438  dfmpq2  7439  enq0enq  7515  nqnq0a  7538  nqnq0m  7539  genpassl  7608  genpassu  7609  axsuploc  8116  recexre  8622  recexgt0  8624  reapmul1  8639  apsqgt0  8645  apreim  8647  recexaplem2  8696  rerecclap  8774  elznn0  9358  elznn  9359  msqznn  9443  eluz2b1  9692  eluz2b3  9695  qreccl  9733  rpnegap  9778  elfz2nn0  10204  elfzo3  10256  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  qexpclz  10669  shftidt2  11014  clim0  11467  iser3shft  11528  summodclem3  11562  fprod2dlemstep  11804  eftlub  11872  ndvdsadd  12113  algfx  12245  isprm3  12311  isprm5  12335  xpsfrnel  13046  isabl2  13500  dvdsrcl2  13731  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  isrim  13801  isnzr2  13816  islmod  13923  isridl  14136  cnfldui  14221  ssntr  14442  tx1cn  14589  tx2cn  14590  pilem1  15099  lgsdir2lem4  15356