ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.32i GIF version

Theorem pm5.32i 435
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.32i.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm5.32i ((𝜑𝜓) ↔ (𝜑𝜒))

Proof of Theorem pm5.32i
StepHypRef Expression
1 pm5.32i.1 . 2 (𝜑 → (𝜓𝜒))
2 pm5.32 434 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 137 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm5.32ri  436  biadan2  437  anbi2i  438  abai  502  anabs5  515  pm5.33  551  eq2tri  2115  rexbiia  2356  reubiia  2511  rmobiia  2516  rabbiia  2564  ceqsrexbv  2698  euxfrdc  2750  dfpss3  3058  eldifsn  3523  elrint  3683  elriin  3755  opeqsn  4017  rabxp  4408  eliunxp  4503  ressn  4886  fncnv  4993  dff1o5  5163  respreima  5323  dff4im  5341  dffo3  5342  f1ompt  5348  fsn  5363  fconst3m  5408  fconst4m  5409  eufnfv  5417  dff13  5435  f1mpt  5438  isores2  5481  isoini  5485  eloprabga  5619  mpt2mptx  5623  resoprab  5625  ov6g  5666  dfopab2  5843  dfoprab3s  5844  dfoprab3  5845  f1od2  5884  brtpos2  5897  dftpos3  5908  tpostpos  5910  dfsmo2  5933  xpcomco  6331  dfplpq2  6510  dfmpq2  6511  enq0enq  6587  nqnq0a  6610  nqnq0m  6611  genpassl  6680  genpassu  6681  recexre  7643  recexgt0  7645  reapmul1  7660  apsqgt0  7666  apreim  7668  recexaplem2  7707  rerecclap  7781  elznn0  8317  elznn  8318  msqznn  8397  eluz2b1  8635  eluz2b3  8638  qreccl  8674  rpnegap  8713  elfz2nn0  9075  elfzo3  9121  frecuzrdgfn  9362  qexpclz  9441  shftidt2  9661  clim0  10037  ndvdsadd  10243  ialgfx  10274
  Copyright terms: Public domain W3C validator