MPE Home 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 239 . 2 (𝜒 → (𝜑𝜓))
32imp 444 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  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 196  df-an 385
This theorem is referenced by:  biantr  968  elrab3t  3330  difprsnss  4270  elpw2g  4754  ideqg  5195  elrnmpt1s  5294  elrnmptg  5296  eqfnfv2  6220  fmpt  6289  elunirn  6413  fun11iun  7019  tposfo2  7262  tposf12  7264  dom2lem  7881  enfii  8062  ssnnfi  8064  ac6sfi  8089  unfilem1  8109  inf3lem2  8409  infdiffi  8438  dfac5lem5  8833  dfac2  8836  dfac12k  8852  cfslb2n  8973  enfin2i  9026  fin23lem19  9041  axdc2lem  9153  axdc3lem4  9158  winainflem  9394  indpi  9608  ltexnq  9676  ltbtwnnq  9679  ltexprlem6  9742  prlem936  9748  elreal2  9832  fimaxre3  10849  addmodlteq  12607  expnbnd  12855  opfi1uzind  13138  opfi1uzindOLD  13144  repswswrd  13382  climcnds  14422  fprod2dlem  14549  fprodle  14566  unbenlem  15450  acsfn  16143  lsmcv  18962  maducoeval2  20265  bastop2  20609  neipeltop  20743  rnelfmlem  21566  isfcls  21623  tgphaus  21730  mbfi1fseqlem4  23291  ulm2  23943  lgsqrmodndvds  24878  2lgsoddprm  24941  ax5seglem5  25613  wlkdvspthlem  26137  wlknwwlknsur  26240  spanunsni  27822  nonbooli  27894  nmopun  28257  lncnopbd  28280  pjnmopi  28391  sumdmdlem  28661  spc2ed  28696  disjun0  28790  rnmpt2ss  28856  esumpcvgval  29467  bnj545  30219  bnj900  30253  bnj1498  30383  soseq  30995  btwnconn1lem7  31370  ivthALT  31500  topfneec  31520  bj-snglss  32151  mptsnunlem  32361  icoreresf  32376  lindsenlbs  32574  matunitlindf  32577  poimirlem14  32593  poimirlem22  32601  poimirlem26  32605  poimirlem29  32608  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  fdc  32711  ismtyres  32777  isdrngo3  32928  lshpset2N  33424  3dimlem1  33762  3dim3  33773  cdleme31fv2  34699  isnumbasgrplem3  36694  pm13.13b  37631  ax6e2ndeqALT  38189  sineq0ALT  38195  elrnmpt1sf  38371  1wlkdlem4  40894  wlknwwlksnsur  41087  31wlkdlem4  41329  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator