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

Theorem pm5.32ri 579
Description: Distribution of implication over biconditional (inference form). (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 578 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
3 ancom 464 . 2 ((𝜓𝜑) ↔ (𝜑𝜓))
4 ancom 464 . 2 ((𝜒𝜑) ↔ (𝜑𝜒))
52, 3, 43bitr4i 306 1 ((𝜓𝜑) ↔ (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  anbi1i  626  pm5.36  832  oranabs  997  pm5.61  998  pm5.75  1026  eu6lem  2636  2eu5  2720  2eu5OLD  2721  ceqsralt  3478  ceqsrexbv  3601  reuind  3695  rabsn  4620  preqsn  4755  reusv2lem4  5270  reusv2lem5  5271  elidinxp  5882  dfoprab2  7195  fsplit  7799  fsplitOLD  7800  xpsnen  8588  elfpw  8814  rankuni  9280  prprrab  13831  isprm2  16019  ismnd  17909  dfgrp2e  18124  pjfval2  20401  neipeltop  21737  cmpfi  22016  isxms2  23058  ishl2  23977  wwlksn0s  27650  clwwlkn1  27829  clwwlkn2  27832  pjimai  29962  bj-snglc  34400  bj-epelb  34480  bj-elid6  34580  isbndx  35213  inecmo2  35763  inecmo3  35768  dfrefrel2  35908  dfcnvrefrel2  35921  dfsymrel2  35938  dfsymrel4  35940  dfsymrel5  35941  refsymrels2  35954  refsymrel2  35956  refsymrel3  35957  dftrrel2  35966  elfunsALTV2  36079  elfunsALTV3  36080  elfunsALTV4  36081  elfunsALTV5  36082  eldisjs2  36109  cdlemefrs29pre00  37684  cdlemefrs29cpre1  37687  dihglb2  38631  elnonrel  40272  pm13.193  41102
  Copyright terms: Public domain W3C validator