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  591  mtbird  597  mtbiri  599  orbi2d  703  pm3.37dc  787  pm5.15dc  1277  exlimd2  1483  exintr  1522  19.9d  1548  19.23t  1564  dral1  1615  spimt  1621  cbvalh  1633  chvar  1637  exdistrfor  1678  sbequi  1717  spv  1737  eqrdav  2036  cleqh  2134  ceqsalg  2576  vtoclf  2601  vtocl2  2603  vtocl3  2604  spcdv  2632  rspcdv  2653  elabgt  2678  sbeqalb  2809  eqrd  2957  copsexg  3972  euotd  3982  rexxfrd  4161  relop  4429  elres  4589  rnxpid  4698  relcnvtr  4783  iotaval  4821  mpteqb  5204  chfnrn  5221  elpreima  5229  ffnfv  5266  f1elima  5355  f1eqcocnv  5374  fliftfun  5379  isoresbr  5392  isotr  5399  ovmpt2dv2  5576  smoiso  5858  nnaordi  6017  nnaword  6020  nnawordi  6024  xpiderm  6113  iinerm  6114  dom2lem  6188  addcanpig  6318  mulcanpig  6319  enqer  6342  ltexnqi  6392  prarloclemlo  6476  genpcdl  6502  genpcuu  6503  appdivnq  6542  ltprordil  6563  1idprl  6564  1idpru  6565  ltexprlemm  6572  ltexprlemopu  6575  ltexprlemru  6584  axpre-ltadd  6730  apne  7367  prodgt02  7560  prodge02  7562  mulgt1  7570  divgt0  7579  divge0  7580  cju  7654  nnsub  7693  nominpos  7899  zltnle  8027  nn0n0n1ge2  8047  zdcle  8053  btwnnz  8070  uzm1  8239  ublbneg  8284  cnref1o  8317  ltsubrp  8352  ltaddrp  8353  ge0nemnf  8467  xltnegi  8478  iccsupr  8565  icoshft  8588  iccshftri  8593  iccshftli  8595  iccdili  8597  icccntri  8599  fzdcel  8634  fznlem  8635  fzen  8637  elfzmlbmOLD  8719  fzofzim  8774  eluzgtdifelfzo  8783  elfzonelfzo  8816  cjre  9070  ch2var  9176  bj-rspgt  9194  bj-nntrans  9339  bj-nnelirr  9341  bj-omtrans  9344  setindft  9349  bj-inf2vnlem3  9356  bj-inf2vnlem4  9357  bj-findis  9363
  Copyright terms: Public domain W3C validator