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

Theorem biimparc 480
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 251 . 2 (𝜒 → (𝜑𝜓))
32imp 407 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  biantr  802  spc2ed  3606  elrab3t  3683  difprsnss  4731  elpw2g  5244  ideqg  5721  elrnmpt1s  5828  elrnmptg  5830  eqfnfv2  6799  fmpt  6870  elunirn  7004  f1iunw  7633  f1iun  7636  tposfo2  7906  tposf12  7908  dom2lem  8538  enfii  8724  ssnnfi  8726  ac6sfi  8751  unfilem1  8771  inf3lem2  9081  infdiffi  9110  dfac5lem5  9542  dfac2b  9545  dfac12k  9562  cfslb2n  9679  enfin2i  9732  fin23lem19  9747  axdc2lem  9859  axdc3lem4  9864  winainflem  10104  indpi  10318  ltexnq  10386  ltbtwnnq  10389  ltexprlem6  10452  prlem936  10458  elreal2  10543  fimaxre3  11576  addmodlteq  13304  expnbnd  13583  opfi1uzind  13849  repswswrd  14136  cshwidxmod  14155  climcnds  15196  fprod2dlem  15324  fprodle  15340  unbenlem  16234  acsfn  16920  lsmcv  19833  maducoeval2  21165  bastop2  21518  neipeltop  21653  rnelfmlem  22476  isfcls  22533  tgphaus  22640  mbfi1fseqlem4  24234  ulm2  24888  lgsqrmodndvds  25843  2lgsoddprm  25906  ax5seglem5  26633  wlkdlem4  27381  clwwlknonwwlknonb  27799  3wlkdlem4  27855  spanunsni  29270  nonbooli  29342  nmopun  29705  lncnopbd  29728  pjnmopi  29839  sumdmdlem  30109  disjun0  30260  rnmposs  30334  esumpcvgval  31223  bnj545  32053  bnj900  32087  bnj1498  32217  soseq  32980  btwnconn1lem7  33438  ivthALT  33567  topfneec  33587  bj-snglss  34166  bj-elpwg  34226  bj-ideqg1ALT  34336  mptsnunlem  34488  icoreresf  34502  lindsenlbs  34754  matunitlindf  34757  poimirlem14  34773  poimirlem22  34781  poimirlem26  34785  poimirlem29  34788  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  fdc  34888  ismtyres  34954  isdrngo3  35105  lshpset2N  36122  3dimlem1  36461  3dim3  36472  cdleme31fv2  37396  isnumbasgrplem3  39570  pm13.13b  40605  ax6e2ndeqALT  41130  sineq0ALT  41136  elrnmpt1sf  41315  requad1  43619  nn0sumshdiglemB  44512
  Copyright terms: Public domain W3C validator