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

Theorem pm5.32i 427
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 426 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 133 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.32ri  428  biadan2  429  anbi2i  430  abai  494  anabs5  507  pm5.33  541  eq2tri  2099  rexbiia  2339  reubiia  2494  rmobiia  2499  rabbiia  2547  ceqsrexbv  2675  euxfrdc  2727  dfpss3  3030  eldifsn  3495  elrint  3655  elriin  3727  opeqsn  3989  rabxp  4380  eliunxp  4475  ressn  4858  fncnv  4965  dff1o5  5135  respreima  5295  dff4im  5313  dffo3  5314  f1ompt  5320  fsn  5335  fconst3m  5380  fconst4m  5381  eufnfv  5389  dff13  5407  f1mpt  5410  isores2  5453  isoini  5457  eloprabga  5591  mpt2mptx  5595  resoprab  5597  ov6g  5638  dfopab2  5815  dfoprab3s  5816  dfoprab3  5817  brtpos2  5866  dftpos3  5877  tpostpos  5879  dfsmo2  5902  xpcomco  6300  dfplpq2  6450  dfmpq2  6451  enq0enq  6527  nqnq0a  6550  nqnq0m  6551  genpassl  6620  genpassu  6621  recexre  7567  recexgt0  7569  reapmul1  7584  apsqgt0  7590  apreim  7592  recexaplem2  7631  rerecclap  7704  elznn0  8258  elznn  8259  msqznn  8336  eluz2b1  8537  eluz2b3  8539  qreccl  8574  rpnegap  8613  elfz2nn0  8971  elfzo3  9017  frecuzrdgfn  9172  qexpclz  9250  shftidt2  9407  clim0  9780  ialgfx  9865
  Copyright terms: Public domain W3C validator