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  2294  rexbiia  2559  reubiia  2732  rmobiia  2737  rabbiia  2801  ceqsrexbv  2951  euxfrdc  3006  eldifpr  3721  eldiftp  3740  eldifsn  3825  elrint  3994  elriin  4067  opeqsn  4374  rabxp  4792  eliunxp  4899  restidsing  5099  ressn  5308  fncnv  5427  dff1o5  5628  respreima  5810  dff4im  5828  dffo3  5829  f1ompt  5833  fsn  5854  fconst3m  5908  fconst4m  5909  eufnfv  5922  dff13  5947  f1mpt  5950  isores2  5992  isoini  5997  eloprabga  6148  mpomptx  6152  resoprab  6157  ov6g  6200  dfopab2  6396  dfoprab3s  6397  dfoprab3  6398  f1od2  6444  brtpos2  6495  dftpos3  6506  tpostpos  6508  dfsmo2  6531  elixp2  6950  mapsnen  7066  xpcomco  7090  eqinfti  7324  dfplpq2  7685  dfmpq2  7686  enq0enq  7762  nqnq0a  7785  nqnq0m  7786  genpassl  7855  genpassu  7856  axsuploc  8362  recexre  8870  recexgt0  8872  reapmul1  8887  apsqgt0  8893  apreim  8895  recexaplem2  8944  rerecclap  9024  elznn0  9612  elznn  9613  msqznn  9699  eluz2b1  9954  eluz2b3  9957  qreccl  9995  rpnegap  10040  elfz2nn0  10471  elfzo3  10523  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  qexpclz  10949  shftidt2  11545  clim0  11999  iser3shft  12060  summodclem3  12095  fprod2dlemstep  12337  eftlub  12405  ndvdsadd  12646  algfx  12778  isprm3  12844  isprm5  12868  ballotfilemodife  13188  xpsfrnel  13612  isabl2  14051  dvdsrcl2  14348  unitinvcl  14372  unitinvinv  14373  unitlinv  14375  unitrinv  14376  isrim  14418  isnzr2  14433  drngprop  14559  islmod  14569  isridl  14782  cnfldui  14867  ssntr  15117  tx1cn  15264  tx2cn  15265  pilem1  15774  lgsdir2lem4  16034