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

Theorem biimpac 501
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 237 . 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:  gencbvex2  3220  2reu5  3379  poltletr  5431  ordnbtwn  5716  ordnbtwnOLD  5717  tz6.12-1  6102  nfunsn  6117  onsucuni2  6900  smo11  7322  omlimcl  7519  omxpenlem  7920  fodomr  7970  fodomfib  8099  r1val1  8506  alephval3  8790  dfac5lem4  8806  dfac5  8808  axdc4lem  9134  fodomb  9203  distrlem1pr  9700  map2psrpr  9784  supsrlem  9785  eqle  9987  swrd0  13229  reuccats1lem  13274  repswswrd  13325  cshwidxmod  13343  rtrclind  13596  sumz  14243  prod1  14456  divalglem8  14904  flodddiv4  14918  pospo  16739  mgm2nsgrplem2  17172  lsmcv  18905  opsrtoslem1  19248  psrbagfsupp  19273  madugsum  20207  hauscmplem  20958  bwth  20962  ptbasfi  21133  hmphindis  21349  fbncp  21392  fgcl  21431  fixufil  21475  uffixfr  21476  mbfima  23119  mbfimaicc  23120  ig1pdvds  23654  zabsle1  24735  tgldimor  25111  ax5seglem4  25527  axcontlem2  25560  axcontlem4  25562  uhgraun  25603  usgfiregdegfi  26201  eupai  26257  usgreghash2spot  26359  numclwwlkun  26369  spansncvi  27698  eigposi  27882  pjnormssi  28214  sumdmdlem  28464  rhmdvdsr  28952  bnj168  29855  bnj521  29862  bnj964  30070  bnj966  30071  bnj1398  30159  cgrdegen  31084  btwnconn1lem11  31177  btwnconn1lem12  31178  btwnconn1lem14  31180  bj-elid3  32064  bj-ccinftydisj  32077  phpreu  32363  fin2so  32366  matunitlindflem2  32376  poimirlem26  32405  poimirlem28  32407  dvasin  32466  isbnd2  32552  atcvrj0  33532  paddasslem5  33928  pm13.13a  37430  iotavalb  37453  suctrALTcf  37980  suctrALTcfVD  37981  suctrALT3  37982  unisnALT  37984  2sb5ndALT  37990  xreqle  38276  fourierdlem40  38841  fourierdlem78  38878  fdisjdmun  39659  funopsn  40141  2ffzoeq  40185  nbgrval  40559  cusgrfi  40673  fusgrregdegfi  40768  rusgr1vtxlem  40786  ifpprsnss  40844  1wlkiswwlksupgr2  41073  elwwlks2ons3  41158  eucrctshift  41410  fusgreghash2wsp  41501  av-numclwlk1lem2f1  41523  difmodm1lt  42110  nn0sumshdiglemA  42210
  Copyright terms: Public domain W3C validator