New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  biimpcd GIF version

Theorem biimpcd 215
 Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimpcd.1 (φ → (ψχ))
Assertion
Ref Expression
biimpcd (ψ → (φχ))

Proof of Theorem biimpcd
StepHypRef Expression
1 id 19 . 2 (ψψ)
2 biimpcd.1 . 2 (φ → (ψχ))
31, 2syl5ibcom 211 1 (ψ → (φχ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  biimpac  472  3impexpbicom  1367  ax16i  2046  ax16ALT2  2048  nfsb4t  2080  nelneq  2451  nelneq2  2452  nelne1  2605  nelne2  2606  nssne1  3327  nssne2  3328  psssstr  3375  difsn  3845  iununi  4050  nnsucelrlem2  4425  nnsucelr  4428  nndisjeq  4429  sfinltfin  4535  mosubopt  4612  phialllem1  4616  nbrne1  4656  nbrne2  4657  chfnrn  5399  fnasrn  5417  ffnfv  5427  f1elima  5474  enprmaplem3  6078  taddc  6229  nclenn  6249  fnfreclem3  6319
 Copyright terms: Public domain W3C validator