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  2237  rexbiia  2492  reubiia  2662  rmobiia  2667  rabbiia  2724  ceqsrexbv  2870  euxfrdc  2925  eldifpr  3621  eldiftp  3640  eldifsn  3721  elrint  3886  elriin  3959  opeqsn  4254  rabxp  4665  eliunxp  4768  restidsing  4965  ressn  5171  fncnv  5284  dff1o5  5472  respreima  5646  dff4im  5664  dffo3  5665  f1ompt  5669  fsn  5690  fconst3m  5737  fconst4m  5738  eufnfv  5749  dff13  5771  f1mpt  5774  isores2  5816  isoini  5821  eloprabga  5964  mpomptx  5968  resoprab  5973  ov6g  6014  dfopab2  6192  dfoprab3s  6193  dfoprab3  6194  f1od2  6238  brtpos2  6254  dftpos3  6265  tpostpos  6267  dfsmo2  6290  elixp2  6704  mapsnen  6813  xpcomco  6828  eqinfti  7021  dfplpq2  7355  dfmpq2  7356  enq0enq  7432  nqnq0a  7455  nqnq0m  7456  genpassl  7525  genpassu  7526  axsuploc  8032  recexre  8537  recexgt0  8539  reapmul1  8554  apsqgt0  8560  apreim  8562  recexaplem2  8611  rerecclap  8689  elznn0  9270  elznn  9271  msqznn  9355  eluz2b1  9603  eluz2b3  9606  qreccl  9644  rpnegap  9688  elfz2nn0  10114  elfzo3  10165  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  qexpclz  10543  shftidt2  10843  clim0  11295  iser3shft  11356  summodclem3  11390  fprod2dlemstep  11632  eftlub  11700  ndvdsadd  11938  algfx  12054  isprm3  12120  isprm5  12144  xpsfrnel  12768  isabl2  13102  dvdsrcl2  13273  unitinvcl  13297  unitinvinv  13298  unitlinv  13300  unitrinv  13301  islmod  13386  ssntr  13661  tx1cn  13808  tx2cn  13809  pilem1  14239  lgsdir2lem4  14471