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

Theorem biimpac 502
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 239 . 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:  gencbvex2  3282  2reu5  3449  ifpprsnss  4331  poltletr  5563  ordnbtwn  5854  ordnbtwnOLD  5855  tz6.12-1  6248  nfunsn  6263  funopsn  6453  onsucuni2  7076  smo11  7506  omlimcl  7703  omxpenlem  8102  fodomr  8152  fodomfib  8281  r1val1  8687  alephval3  8971  dfac5lem4  8987  dfac5  8989  axdc4lem  9315  fodomb  9386  distrlem1pr  9885  map2psrpr  9969  supsrlem  9970  eqle  10177  ccat1st1st  13448  swrd0  13480  reuccats1lem  13525  repswswrd  13577  cshwidxmod  13595  rtrclind  13849  sumz  14497  prod1  14718  divalglem8  15170  flodddiv4  15184  pospo  17020  mgm2nsgrplem2  17453  lsmcv  19189  opsrtoslem1  19532  psrbagfsupp  19557  madugsum  20497  hauscmplem  21257  bwth  21261  ptbasfi  21432  hmphindis  21648  fbncp  21690  fgcl  21729  fixufil  21773  uffixfr  21774  mbfima  23444  mbfimaicc  23445  ig1pdvds  23981  zabsle1  25066  tgldimor  25442  ax5seglem4  25857  axcontlem2  25890  axcontlem4  25892  nbgrval  26274  cusgrfi  26410  fusgrregdegfi  26521  rusgr1vtxlem  26539  wlkiswwlksupgr2  26831  elwwlks2ons3  26920  elwwlks2ons3OLD  26921  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  eucrctshift  27221  spansncvi  28639  eigposi  28823  pjnormssi  29155  sumdmdlem  29405  rhmdvdsr  29946  bnj168  30924  bnj521  30931  bnj964  31139  bnj966  31140  bnj1398  31228  cgrdegen  32236  btwnconn1lem11  32329  btwnconn1lem12  32330  btwnconn1lem14  32332  bj-elid3  33217  bj-ccinftydisj  33230  phpreu  33523  fin2so  33526  matunitlindflem2  33536  poimirlem26  33565  poimirlem28  33567  dvasin  33626  isbnd2  33712  atcvrj0  35032  paddasslem5  35428  pm13.13a  38925  iotavalb  38948  suctrALTcf  39472  suctrALTcfVD  39473  suctrALT3  39474  unisnALT  39476  2sb5ndALT  39482  xreqle  39847  supminfxr2  40012  fourierdlem40  40682  fourierdlem78  40719  2ffzoeq  41663  uspgropssxp  42077  uspgrsprfo  42081  difmodm1lt  42642  nn0sumshdiglemA  42738
  Copyright terms: Public domain W3C validator