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

Theorem pm5.32ri 668
 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 667 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
3 ancom 465 . 2 ((𝜓𝜑) ↔ (𝜑𝜓))
4 ancom 465 . 2 ((𝜒𝜑) ↔ (𝜑𝜒))
52, 3, 43bitr4i 291 1 ((𝜓𝜑) ↔ (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  anbi1i  727  pm5.61  745  oranabs  897  pm5.36  919  pm5.75  974  2eu5  2545  ceqsralt  3202  ceqsrexbv  3307  reuind  3378  rabsn  4200  preqsn  4331  reusv2lem4  4798  reusv2lem5  4799  dfoprab2  6599  fsplit  7169  xpsnen  7929  elfpw  8151  rankuni  8609  prprrab  13112  isprm2  15233  ismnd  17120  dfgrp2e  17271  pjfval2  19872  neipeltop  20743  cmpfi  21021  isxms2  22063  ishl2  22974  usgraop  25879  pjimai  28419  bj-snglc  32150  isbndx  32751  cdlemefrs29pre00  34701  cdlemefrs29cpre1  34704  dihglb2  35649  elnonrel  36910  pm13.193  37634  wwlksn0s  41057  clwwlksn2  41217
 Copyright terms: Public domain W3C validator