MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimparc Structured version   Visualization version   GIF version

Theorem biimparc 471
Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimparc ((𝜒𝜑) → 𝜓)

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimprcd 241 . 2 (𝜒 → (𝜑𝜓))
32imp 395 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  biantr  840  elrab3t  3518  difprsnss  4484  elpw2g  4985  ideqg  5442  elrnmpt1s  5542  elrnmptg  5544  eqfnfv2  6502  fmpt  6570  elunirn  6701  fun11iun  7324  tposfo2  7578  tposf12  7580  dom2lem  8200  enfii  8384  ssnnfi  8386  ac6sfi  8411  unfilem1  8431  inf3lem2  8741  infdiffi  8770  dfac5lem5  9201  dfac2b  9204  dfac2OLD  9206  dfac12k  9222  cfslb2n  9343  enfin2i  9396  fin23lem19  9411  axdc2lem  9523  axdc3lem4  9528  winainflem  9768  indpi  9982  ltexnq  10050  ltbtwnnq  10053  ltexprlem6  10116  prlem936  10122  elreal2  10206  fimaxre3  11224  addmodlteq  12953  expnbnd  13200  opfi1uzind  13484  repswswrd  13808  climcnds  14867  fprod2dlem  14993  fprodle  15009  unbenlem  15891  acsfn  16585  lsmcv  19414  maducoeval2  20723  bastop2  21078  neipeltop  21213  rnelfmlem  22035  isfcls  22092  tgphaus  22199  mbfi1fseqlem4  23776  ulm2  24430  lgsqrmodndvds  25369  2lgsoddprm  25432  ax5seglem5  26104  wlkdlem4  26874  wlknwwlksnsurOLD  27082  3wlkdlem4  27440  spanunsni  28894  nonbooli  28966  nmopun  29329  lncnopbd  29352  pjnmopi  29463  sumdmdlem  29733  spc2ed  29768  disjun0  29856  rnmpt2ss  29922  esumpcvgval  30587  bnj545  31413  bnj900  31447  bnj1498  31577  soseq  32198  btwnconn1lem7  32644  ivthALT  32773  topfneec  32793  bj-snglss  33385  bj-ismoored  33490  mptsnunlem  33619  icoreresf  33633  lindsenlbs  33828  matunitlindf  33831  poimirlem14  33847  poimirlem22  33855  poimirlem26  33859  poimirlem29  33862  ovoliunnfl  33875  voliunnfl  33877  volsupnfl  33878  fdc  33963  ismtyres  34029  isdrngo3  34180  lshpset2N  35075  3dimlem1  35414  3dim3  35425  cdleme31fv2  36349  isnumbasgrplem3  38352  pm13.13b  39282  ax6e2ndeqALT  39819  sineq0ALT  39825  elrnmpt1sf  40023  nn0sumshdiglemB  43083
  Copyright terms: Public domain W3C validator