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 576
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 575 . 2 ((𝜑𝜓) ↔ (𝜑𝜒))
3 ancom 461 . 2 ((𝜓𝜑) ↔ (𝜑𝜓))
4 ancom 461 . 2 ((𝜒𝜑) ↔ (𝜑𝜒))
52, 3, 43bitr4i 304 1 ((𝜓𝜑) ↔ (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  anbi1i  623  pm5.36  829  oranabs  993  pm5.61  994  pm5.75  1022  eu6lem  2651  2eu5  2735  2eu5OLD  2736  ceqsralt  3526  ceqsrexbv  3647  reuind  3741  rabsn  4649  preqsn  4784  reusv2lem4  5292  reusv2lem5  5293  elidinxp  5904  dfoprab2  7201  fsplit  7801  fsplitOLD  7802  xpsnen  8589  elfpw  8814  rankuni  9280  prprrab  13819  isprm2  16014  ismnd  17902  dfgrp2e  18067  pjfval2  20781  neipeltop  21665  cmpfi  21944  isxms2  22985  ishl2  23900  wwlksn0s  27566  clwwlkn1  27746  clwwlkn2  27749  pjimai  29880  bj-snglc  34178  bj-epelb  34255  bj-elid6  34354  isbndx  34941  inecmo2  35491  inecmo3  35496  dfrefrel2  35635  dfcnvrefrel2  35648  dfsymrel2  35665  dfsymrel4  35667  dfsymrel5  35668  refsymrels2  35681  refsymrel2  35683  refsymrel3  35684  dftrrel2  35693  elfunsALTV2  35806  elfunsALTV3  35807  elfunsALTV4  35808  elfunsALTV5  35809  eldisjs2  35836  cdlemefrs29pre00  37411  cdlemefrs29cpre1  37414  dihglb2  38358  elnonrel  39823  pm13.193  40620
  Copyright terms: Public domain W3C validator