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

Theorem biimpd 132
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpd.1 (φ → (ψχ))
Assertion
Ref Expression
biimpd (φ → (ψχ))

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2 (φ → (ψχ))
2 bi1 111 . 2 ((ψχ) → (ψχ))
31, 2syl 14 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
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbid  135  sylibd  138  sylbid  139  mpbidi  140  syl5ib  143  syl6bi  152  ibi  165  imbi1d  220  biimpa  280  notbid  579  mtbird  585  mtbiri  587  orbi2d  691  pm3.37dc  781  pm5.15dc  1263  exlimd2  1468  exintr  1507  19.9d  1533  19.23t  1549  dral1  1600  spimt  1606  cbvalh  1618  chvar  1622  exdistrfor  1663  sbequi  1702  spv  1722  eqrdav  2021  cleqh  2119  ceqsalg  2559  vtoclf  2584  vtocl2  2586  vtocl3  2587  spcdv  2615  rspcdv  2636  elabgt  2661  sbeqalb  2792  eqrd  2940  copsexg  3955  euotd  3965  rexxfrd  4145  relop  4413  elres  4573  rnxpid  4682  relcnvtr  4767  iotaval  4805  mpteqb  5186  chfnrn  5203  elpreima  5211  ffnfv  5248  f1elima  5337  f1eqcocnv  5356  fliftfun  5361  isoresbr  5374  isotr  5381  ovmpt2dv2  5557  smoiso  5839  nnaordi  5992  nnaword  5995  nnawordi  5999  xpiderm  6088  iinerm  6089  addcanpig  6194  mulcanpig  6195  enqer  6217  prarloclemlo  6348  genpcdl  6374  genpcuu  6375  appdivnq  6407  prmuloc  6410  ltprordil  6428  1idprl  6429  1idpru  6430  ltexprlemm  6437  ltexprlemopu  6440  ltexprlemloc  6444  ltexprlemru  6449  addcanprlemu  6452  axpre-ltadd  6579  ch2var  7014  bj-rspgt  7032  bj-nntrans  7173  bj-nnelirr  7175  bj-omtrans  7178  setindft  7183  bj-inf2vnlem3  7190  bj-inf2vnlem4  7191  bj-findis  7197
  Copyright terms: Public domain W3C validator