ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicomd Structured version   GIF version

Theorem bicomd 129
Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomd.1 (φ → (ψχ))
Assertion
Ref Expression
bicomd (φ → (χψ))

Proof of Theorem bicomd
StepHypRef Expression
1 bicomd.1 . 2 (φ → (ψχ))
2 bicom 128 . 2 ((ψχ) ↔ (χψ))
31, 2sylib 127 1 (φ → (χψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  impbid2  131  syl5ibr  145  ibir  166  bitr2d  178  bitr3d  179  bitr4d  180  syl5rbb  182  syl6rbb  186  pm5.5  231  anabs5  492  con2bidc  753  con1biidc  755  con2biidc  757  pm4.63dc  764  pm4.64dc  785  pm5.55dc  803  baibr  813  pm4.55dc  828  anordc  845  pm5.75  851  ninba  861  xor3dc  1256  3impexpbicomi  1301  cbvexh  1611  sbequ12r  1628  sbco  1815  sbcomxyyz  1819  sbal1yz  1850  cbvab  2133  nnedc  2184  necon3bbid  2214  necon2abiidc  2238  necon2bbii  2239  gencbvex  2568  gencbval  2570  sbhypf  2571  clel3g  2646  reu8  2705  sbceq2a  2742  sbcco2  2754  sbcsng  3392  opabid  3957  soeq2  4016  tfisi  4225  posng  4327  xpiindim  4388  fvopab6  5177  fconstfvm  5292  cbvfo  5338  cbvexfo  5339  f1eqcocnv  5344  isoid  5363  isoini  5370  resoprab2  5509  dfoprab3  5728  nnacan  5984  nnmcan  5991  dfmpq2  6200  ztri3or  7861  nn0ind-raph  7919  zindd  7920  qreccl  8057  bj-indeq  8314
  Copyright terms: Public domain W3C validator