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  6501  genpcuu  6502  appdivnq  6543  ltprordil  6564  1idprl  6565  1idpru  6566  ltexprlemm  6573  ltexprlemopu  6576  ltexprlemru  6585  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  axpre-ltadd  6750  apne  7387  prodgt02  7580  prodge02  7582  mulgt1  7590  divgt0  7599  divge0  7600  cju  7674  nnsub  7713  nominpos  7919  zltnle  8047  nn0n0n1ge2  8067  zdcle  8073  btwnnz  8090  uzm1  8259  ublbneg  8304  cnref1o  8337  ltsubrp  8372  ltaddrp  8373  ge0nemnf  8487  xltnegi  8498  iccsupr  8585  icoshft  8608  iccshftri  8613  iccshftli  8615  iccdili  8617  icccntri  8619  fzdcel  8654  fznlem  8655  fzen  8657  elfzmlbmOLD  8739  fzofzim  8794  eluzgtdifelfzo  8803  elfzonelfzo  8836  cjre  9090  ch2var  9222  bj-rspgt  9240  bj-nntrans  9385  bj-nnelirr  9387  bj-omtrans  9390  setindft  9395  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403  bj-findis  9409
  Copyright terms: Public domain W3C validator