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

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

Proof of Theorem biimpac
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpcd 249 . 2 (𝜓 → (𝜑𝜒))
32imp 408 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  r19.29r  3118  gencbvex2  3504  2reu5  3715  ifpprsnss  4724  dfiun2g  4989  poltletr  6083  ordnbtwn  6407  tz6.12-1OLD  6862  funopsn  7089  onsucuni2  7760  1stconst  8021  2ndconst  8022  smo11  8278  omlimcl  8493  omxpenlem  8951  fodomr  9006  f1oenfirn  9061  f1domfi  9062  fodomfib  9204  infsupprpr  9374  r1val1  9656  alephval3  9980  dfac5lem4  9996  dfac5  9998  axdc4lem  10325  fodomb  10396  distrlem1pr  10895  map2psrpr  10980  supsrlem  10981  eqle  11191  swrd0  14479  repswswrd  14605  cshwidxmod  14624  rtrclind  14885  sumz  15543  prod1  15763  divalglem8  16218  flodddiv4  16231  pospo  18170  mgm2nsgrplem2  18665  rhmdvdsr  20110  lsmcv  20531  psrbagfsuppOLD  21252  opsrtoslem1  21390  madugsum  21920  hauscmplem  22685  bwth  22689  ptbasfi  22860  hmphindis  23076  fbncp  23118  fgcl  23157  fixufil  23201  uffixfr  23202  mbfima  24922  mbfimaicc  24923  ig1pdvds  25469  zabsle1  26572  tgldimor  27249  ax5seglem4  27686  axcontlem2  27719  axcontlem4  27721  nbgrval  28089  cusgrfi  28211  fusgrregdegfi  28322  rusgr1vtxlem  28340  wlkiswwlksupgr2  28627  elwwlks2ons3  28705  clwwlknonwwlknonb  28855  eucrctshift  28992  spansncvi  30399  eigposi  30583  pjnormssi  30915  sumdmdlem  31165  sraring  32076  tngdim  32100  bnj168  33122  bnj964  33335  bnj966  33336  bnj1398  33426  fnrelpredd  33473  lfuhgr3  33493  acycgrislfgr  33526  cgrdegen  34520  btwnconn1lem11  34613  btwnconn1lem12  34614  btwnconn1lem14  34616  bj-opelidb1  35555  bj-inexeqex  35556  bj-idreseqb  35565  bj-ideqg1ALT  35567  bj-ccinftydisj  35615  phpreu  35993  fin2so  35996  matunitlindflem2  36006  poimirlem26  36035  poimirlem28  36037  dvasin  36093  isbnd2  36173  atcvrj0  37822  paddasslem5  38218  pm13.13a  42488  iotavalb  42511  suctrALTcf  43005  suctrALTcfVD  43006  suctrALT3  43007  unisnALT  43009  2sb5ndALT  43015  xreqle  43347  supminfxr2  43499  fourierdlem40  44179  fourierdlem78  44216  tz6.12-afv2  45263  afv2fv0  45288  2ffzoeq  45351  uspgropssxp  45837  uspgrsprfo  45841  difmodm1lt  46399  nn0sumshdiglemA  46496  itscnhlc0yqe  46636
  Copyright terms: Public domain W3C validator