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  7440  dfmpq2  7441  enq0enq  7517  nqnq0a  7540  nqnq0m  7541  genpassl  7610  genpassu  7611  axsuploc  8118  recexre  8624  recexgt0  8626  reapmul1  8641  apsqgt0  8647  apreim  8649  recexaplem2  8698  rerecclap  8776  elznn0  9360  elznn  9361  msqznn  9445  eluz2b1  9694  eluz2b3  9697  qreccl  9735  rpnegap  9780  elfz2nn0  10206  elfzo3  10258  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  qexpclz  10671  shftidt2  11016  clim0  11469  iser3shft  11530  summodclem3  11564  fprod2dlemstep  11806  eftlub  11874  ndvdsadd  12115  algfx  12247  isprm3  12313  isprm5  12337  xpsfrnel  13048  isabl2  13502  dvdsrcl2  13733  unitinvcl  13757  unitinvinv  13758  unitlinv  13760  unitrinv  13761  isrim  13803  isnzr2  13818  islmod  13925  isridl  14138  cnfldui  14223  ssntr  14466  tx1cn  14613  tx2cn  14614  pilem1  15123  lgsdir2lem4  15380