ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.32i Structured version   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  2096  rexbiia  2333  reubiia  2488  rmobiia  2493  rabbiia  2541  ceqsrexbv  2669  euxfrdc  2721  dfpss3  3024  eldifsn  3486  elrint  3646  elriin  3718  opeqsn  3980  rabxp  4323  eliunxp  4418  ressn  4801  fncnv  4908  dff1o5  5078  respreima  5238  dff4im  5256  dffo3  5257  f1ompt  5263  fsn  5278  fconst3m  5323  fconst4m  5324  eufnfv  5332  dff13  5350  f1mpt  5353  isores2  5396  isoini  5400  eloprabga  5533  mpt2mptx  5537  resoprab  5539  ov6g  5580  dfopab2  5757  dfoprab3s  5758  dfoprab3  5759  brtpos2  5807  dftpos3  5818  tpostpos  5820  dfsmo2  5843  xpcomco  6236  dfplpq2  6338  dfmpq2  6339  enq0enq  6413  nqnq0a  6436  nqnq0m  6437  genpassl  6506  genpassu  6507  recexre  7342  recexgt0  7344  reapmul1  7359  apsqgt0  7365  apreim  7367  recexaplem2  7395  rerecclap  7468  elznn0  8016  elznn  8017  msqznn  8094  eluz2b1  8295  eluz2b3  8297  qreccl  8331  rpnegap  8370  elfz2nn0  8723  elfzo3  8769  frecuzrdgfn  8859  qexpclz  8910
  Copyright terms: Public domain W3C validator