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

Theorem pm5.32ri 673
 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 672 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
3 ancom 465 . 2 ((𝜓𝜑) ↔ (𝜑𝜓))
4 ancom 465 . 2 ((𝜒𝜑) ↔ (𝜑𝜒))
52, 3, 43bitr4i 292 1 ((𝜓𝜑) ↔ (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ 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 197  df-an 385 This theorem is referenced by:  anbi1i  733  pm5.61  751  oranabs  937  pm5.36  959  pm5.75  1016  2eu5  2696  ceqsralt  3370  ceqsrexbv  3477  reuind  3553  rabsn  4401  preqsn  4541  preqsnOLD  4542  reusv2lem4  5022  reusv2lem5  5023  dfoprab2  6868  fsplit  7452  xpsnen  8212  elfpw  8436  rankuni  8902  prprrab  13468  isprm2  15618  ismnd  17519  dfgrp2e  17670  pjfval2  20276  neipeltop  21156  cmpfi  21434  isxms2  22475  ishl2  23387  wwlksn0s  26992  clwwlkn1  27192  clwwlkn2  27195  pjimai  29366  bj-snglc  33282  isbndx  33913  inecmo2  34463  inecmo3  34468  dfrefrel2  34607  dfcnvrefrel2  34620  dfsymrel2  34637  dfsymrel4  34639  dfsymrel5  34640  refsymrels2  34653  refsymrel2  34655  refsymrel3  34656  cdlemefrs29pre00  36204  cdlemefrs29cpre1  36207  dihglb2  37152  elnonrel  38412  pm13.193  39133
 Copyright terms: Public domain W3C validator