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

Theorem biimparc 503
 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 240 . 2 (𝜒 → (𝜑𝜓))
32imp 444 1 ((𝜒𝜑) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  biantr  992  elrab3t  3395  difprsnss  4361  elpw2g  4857  ideqg  5306  elrnmpt1s  5405  elrnmptg  5407  eqfnfv2  6352  fmpt  6421  elunirn  6549  fun11iun  7168  tposfo2  7420  tposf12  7422  dom2lem  8037  enfii  8218  ssnnfi  8220  ac6sfi  8245  unfilem1  8265  inf3lem2  8564  infdiffi  8593  dfac5lem5  8988  dfac2  8991  dfac12k  9007  cfslb2n  9128  enfin2i  9181  fin23lem19  9196  axdc2lem  9308  axdc3lem4  9313  winainflem  9553  indpi  9767  ltexnq  9835  ltbtwnnq  9838  ltexprlem6  9901  prlem936  9907  elreal2  9991  fimaxre3  11008  addmodlteq  12785  expnbnd  13033  opfi1uzind  13321  repswswrd  13577  climcnds  14627  fprod2dlem  14754  fprodle  14771  unbenlem  15659  acsfn  16367  lsmcv  19189  maducoeval2  20494  bastop2  20846  neipeltop  20981  rnelfmlem  21803  isfcls  21860  tgphaus  21967  mbfi1fseqlem4  23530  ulm2  24184  lgsqrmodndvds  25123  2lgsoddprm  25186  ax5seglem5  25858  wlkdlem4  26638  wlknwwlksnsur  26844  3wlkdlem4  27140  spanunsni  28566  nonbooli  28638  nmopun  29001  lncnopbd  29024  pjnmopi  29135  sumdmdlem  29405  spc2ed  29440  disjun0  29534  rnmpt2ss  29601  esumpcvgval  30268  bnj545  31091  bnj900  31125  bnj1498  31255  soseq  31879  btwnconn1lem7  32325  ivthALT  32455  topfneec  32475  bj-snglss  33083  bj-ismoored  33187  mptsnunlem  33315  icoreresf  33330  lindsenlbs  33534  matunitlindf  33537  poimirlem14  33553  poimirlem22  33561  poimirlem26  33565  poimirlem29  33568  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  fdc  33671  ismtyres  33737  isdrngo3  33888  lshpset2N  34724  3dimlem1  35062  3dim3  35073  cdleme31fv2  35998  isnumbasgrplem3  37992  pm13.13b  38926  ax6e2ndeqALT  39481  sineq0ALT  39487  elrnmpt1sf  39690  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator