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  3794  elrint  3962  elriin  4035  opeqsn  4338  rabxp  4753  eliunxp  4858  restidsing  5057  ressn  5265  fncnv  5383  dff1o5  5577  respreima  5756  dff4im  5774  dffo3  5775  f1ompt  5779  fsn  5800  fconst3m  5851  fconst4m  5852  eufnfv  5863  dff13  5885  f1mpt  5888  isores2  5930  isoini  5935  eloprabga  6082  mpomptx  6086  resoprab  6091  ov6g  6134  dfopab2  6325  dfoprab3s  6326  dfoprab3  6327  f1od2  6371  brtpos2  6387  dftpos3  6398  tpostpos  6400  dfsmo2  6423  elixp2  6839  mapsnen  6954  xpcomco  6973  eqinfti  7175  dfplpq2  7529  dfmpq2  7530  enq0enq  7606  nqnq0a  7629  nqnq0m  7630  genpassl  7699  genpassu  7700  axsuploc  8207  recexre  8713  recexgt0  8715  reapmul1  8730  apsqgt0  8736  apreim  8738  recexaplem2  8787  rerecclap  8865  elznn0  9449  elznn  9450  msqznn  9535  eluz2b1  9784  eluz2b3  9787  qreccl  9825  rpnegap  9870  elfz2nn0  10296  elfzo3  10348  frecuzrdgtcl  10621  frecuzrdgfunlem  10628  qexpclz  10769  shftidt2  11329  clim0  11782  iser3shft  11843  summodclem3  11877  fprod2dlemstep  12119  eftlub  12187  ndvdsadd  12428  algfx  12560  isprm3  12626  isprm5  12650  xpsfrnel  13363  isabl2  13817  dvdsrcl2  14048  unitinvcl  14072  unitinvinv  14073  unitlinv  14075  unitrinv  14076  isrim  14118  isnzr2  14133  islmod  14240  isridl  14453  cnfldui  14538  ssntr  14781  tx1cn  14928  tx2cn  14929  pilem1  15438  lgsdir2lem4  15695