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

Theorem pm5.32i 442
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 441 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 143 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.32ri  443  biadan2  444  anbi2i  445  abai  525  anabs5  538  pm5.33  574  eq2tri  2144  rexbiia  2389  reubiia  2547  rmobiia  2552  rabbiia  2600  ceqsrexbv  2739  euxfrdc  2792  eldifsn  3552  elrint  3713  elriin  3785  opeqsn  4055  rabxp  4448  eliunxp  4545  ressn  4939  fncnv  5047  dff1o5  5227  respreima  5392  dff4im  5410  dffo3  5411  f1ompt  5415  fsn  5434  fconst3m  5479  fconst4m  5480  eufnfv  5488  dff13  5510  f1mpt  5513  isores2  5555  isoini  5560  eloprabga  5694  mpt2mptx  5698  resoprab  5700  ov6g  5741  dfopab2  5918  dfoprab3s  5919  dfoprab3  5920  f1od2  5959  brtpos2  5972  dftpos3  5983  tpostpos  5985  dfsmo2  6008  mapsnen  6482  xpcomco  6496  eqinfti  6662  dfplpq2  6860  dfmpq2  6861  enq0enq  6937  nqnq0a  6960  nqnq0m  6961  genpassl  7030  genpassu  7031  recexre  7999  recexgt0  8001  reapmul1  8016  apsqgt0  8022  apreim  8024  recexaplem2  8063  rerecclap  8139  elznn0  8701  elznn  8702  msqznn  8782  eluz2b1  9023  eluz2b3  9026  qreccl  9062  rpnegap  9101  elfz2nn0  9459  elfzo3  9505  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  qexpclz  9878  shftidt2  10166  clim0  10571  isummolem3  10664  ndvdsadd  10837  ialgfx  10940  isprm3  11006
  Copyright terms: Public domain W3C validator