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  6414  nqnq0a  6437  nqnq0m  6438  genpassl  6507  genpassu  6508  recexre  7362  recexgt0  7364  reapmul1  7379  apsqgt0  7385  apreim  7387  recexaplem2  7415  rerecclap  7488  elznn0  8036  elznn  8037  msqznn  8114  eluz2b1  8315  eluz2b3  8317  qreccl  8351  rpnegap  8390  elfz2nn0  8743  elfzo3  8789  frecuzrdgfn  8879  qexpclz  8930
  Copyright terms: Public domain W3C validator