Theorem pm5.32i 458

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 457	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 145	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32ri  459  biadan2  460  anbi2i  461  abai  566  anabs5  579  pm5.33  617  annotanannot  680  eq2tri  2298  rexbiia  2565  reubiia  2738  rmobiia  2743  rabbiia  2807  ceqsrexbv  2957  euxfrdc  3012  eldifpr  3736  eldiftp  3755  eldifsn  3841  elrint  4010  elriin  4083  opeqsn  4395  rabxp  4814  eliunxp  4921  restidsing  5122  ressn  5331  fncnv  5450  dff1o5  5651  respreima  5839  dff4im  5857  dffo3  5858  f1ompt  5862  fsn  5883  fconst3m  5937  fconst4m  5938  eufnfv  5952  dff13  5977  f1mpt  5980  isores2  6022  isoini  6027  eloprabga  6178  mpomptx  6182  resoprab  6187  ov6g  6230  dfopab2  6427  dfoprab3s  6428  dfoprab3  6429  f1od2  6475  brtpos2  6526  dftpos3  6537  tpostpos  6539  dfsmo2  6562  elixp2  6989  mapsnen  7105  xpcomco  7129  eqinfti  7367  dfplpq2  7728  dfmpq2  7729  enq0enq  7805  nqnq0a  7828  nqnq0m  7829  genpassl  7898  genpassu  7899  axsuploc  8405  recexre  8915  recexgt0  8917  reapmul1  8932  apsqgt0  8938  apreim  8940  recexaplem2  8989  rerecclap  9069  elznn0  9671  elznn  9672  msqznn  9758  eluz2b1  10018  eluz2b3  10021  qreccl  10059  rpnegap  10105  elfz2nn0  10537  elfzo3  10589  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  qexpclz  11019  shftidt2  11620  clim0  12077  iser3shft  12138  summodclem3  12173  fprod2dlemstep  12415  eftlub  12483  ndvdsadd  12724  algfx  12856  isprm3  12922  isprm5  12947  ballotfilemodife  13299  xpsfrnel  13725  isabl2  14188  dvdsrcl2  14516  unitinvcl  14540  unitinvinv  14541  unitlinv  14543  unitrinv  14544  isrim  14586  isnzr2  14601  drngprop  14727  islmod  14737  isridl  14951  cnfldui  15034  isassa  15112  ssntr  15360  tx1cn  15507  tx2cn  15508  pilem1  16018  lgsdir2lem4  16367  alsralrex  17372  dfalseu2  17396