Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32ri Structured version   Visualization version   GIF version

Theorem pm5.32ri 669
 Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)
Hypothesis
Ref Expression
pm5.32i.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm5.32ri ((𝜓𝜑) ↔ (𝜒𝜑))

Proof of Theorem pm5.32ri
StepHypRef Expression
1 pm5.32i.1 . . 3 (𝜑 → (𝜓𝜒))
21pm5.32i 668 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
3 ancom 466 . 2 ((𝜓𝜑) ↔ (𝜑𝜓))
4 ancom 466 . 2 ((𝜒𝜑) ↔ (𝜑𝜒))
52, 3, 43bitr4i 292 1 ((𝜓𝜑) ↔ (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 386 This theorem is referenced by:  anbi1i  730  pm5.61  748  oranabs  900  pm5.36  922  pm5.75  977  2eu5  2556  ceqsralt  3215  ceqsrexbv  3320  reuind  3393  rabsn  4226  preqsn  4361  reusv2lem4  4832  reusv2lem5  4833  dfoprab2  6654  fsplit  7227  xpsnen  7988  elfpw  8212  rankuni  8670  prprrab  13193  isprm2  15319  ismnd  17218  dfgrp2e  17369  pjfval2  19972  neipeltop  20843  cmpfi  21121  isxms2  22163  ishl2  23074  wwlksn0s  26615  clwwlksn2  26776  pjimai  28884  bj-snglc  32604  isbndx  33213  cdlemefrs29pre00  35163  cdlemefrs29cpre1  35166  dihglb2  36111  elnonrel  37372  pm13.193  38094
 Copyright terms: Public domain W3C validator