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  3649  eldiftp  3668  eldifsn  3749  elrint  3914  elriin  3987  opeqsn  4285  rabxp  4700  eliunxp  4805  restidsing  5002  ressn  5210  fncnv  5324  dff1o5  5513  respreima  5690  dff4im  5708  dffo3  5709  f1ompt  5713  fsn  5734  fconst3m  5781  fconst4m  5782  eufnfv  5793  dff13  5815  f1mpt  5818  isores2  5860  isoini  5865  eloprabga  6009  mpomptx  6013  resoprab  6018  ov6g  6061  dfopab2  6247  dfoprab3s  6248  dfoprab3  6249  f1od2  6293  brtpos2  6309  dftpos3  6320  tpostpos  6322  dfsmo2  6345  elixp2  6761  mapsnen  6870  xpcomco  6885  eqinfti  7086  dfplpq2  7421  dfmpq2  7422  enq0enq  7498  nqnq0a  7521  nqnq0m  7522  genpassl  7591  genpassu  7592  axsuploc  8099  recexre  8605  recexgt0  8607  reapmul1  8622  apsqgt0  8628  apreim  8630  recexaplem2  8679  rerecclap  8757  elznn0  9341  elznn  9342  msqznn  9426  eluz2b1  9675  eluz2b3  9678  qreccl  9716  rpnegap  9761  elfz2nn0  10187  elfzo3  10239  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  qexpclz  10652  shftidt2  10997  clim0  11450  iser3shft  11511  summodclem3  11545  fprod2dlemstep  11787  eftlub  11855  ndvdsadd  12096  algfx  12220  isprm3  12286  isprm5  12310  xpsfrnel  12987  isabl2  13424  dvdsrcl2  13655  unitinvcl  13679  unitinvinv  13680  unitlinv  13682  unitrinv  13683  isrim  13725  isnzr2  13740  islmod  13847  isridl  14060  cnfldui  14145  ssntr  14358  tx1cn  14505  tx2cn  14506  pilem1  15015  lgsdir2lem4  15272