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

Theorem biimparc 502
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 238 . 2 (𝜒 → (𝜑𝜓))
32imp 443 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  biantr  967  elrab3t  3329  difprsnss  4269  elpw2g  4749  ideqg  5183  elrnmpt1s  5281  elrnmptg  5283  eqfnfv2  6205  fmpt  6274  elunirn  6391  fun11iun  6996  tposfo2  7239  tposf12  7241  dom2lem  7858  enfii  8039  ssnnfi  8041  ac6sfi  8066  unfilem1  8086  inf3lem2  8386  infdiffi  8415  dfac5lem5  8810  dfac2  8813  dfac12k  8829  cfslb2n  8950  enfin2i  9003  fin23lem19  9018  axdc2lem  9130  axdc3lem4  9135  winainflem  9371  indpi  9585  ltexnq  9653  ltbtwnnq  9656  ltexprlem6  9719  prlem936  9725  elreal2  9809  fimaxre3  10819  addmodlteq  12562  expnbnd  12810  opfi1uzind  13084  opfi1uzindOLD  13090  repswswrd  13328  climcnds  14368  fprod2dlem  14495  fprodle  14512  unbenlem  15396  acsfn  16089  lsmcv  18908  maducoeval2  20207  bastop2  20551  neipeltop  20685  rnelfmlem  21508  isfcls  21565  tgphaus  21672  mbfi1fseqlem4  23208  ulm2  23860  lgsqrmodndvds  24795  2lgsoddprm  24858  ax5seglem5  25531  wlkdvspthlem  25903  wlknwwlknsur  26006  spanunsni  27628  nonbooli  27700  nmopun  28063  lncnopbd  28086  pjnmopi  28197  sumdmdlem  28467  spc2ed  28502  disjun0  28596  rnmpt2ss  28662  esumpcvgval  29273  bnj545  30025  bnj900  30059  bnj1498  30189  soseq  30801  btwnconn1lem7  31176  ivthALT  31306  topfneec  31326  bj-snglss  31947  mptsnunlem  32157  icoreresf  32172  lindsenlbs  32370  matunitlindf  32373  poimirlem14  32389  poimirlem22  32397  poimirlem26  32401  poimirlem29  32404  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  fdc  32507  ismtyres  32573  isdrngo3  32724  lshpset2N  33220  3dimlem1  33558  3dim3  33569  cdleme31fv2  34495  isnumbasgrplem3  36490  pm13.13b  37427  ax6e2ndeqALT  37985  sineq0ALT  37991  elrnmpt1sf  38167  1wlkdlem4  40889  wlknwwlksnsur  41082  31wlkdlem4  41324  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator