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 238 . 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:  gencbvex2  3224  2reu5  3383  poltletr  5447  ordnbtwn  5733  ordnbtwnOLD  5734  tz6.12-1  6120  nfunsn  6135  funopsn  6319  onsucuni2  6926  smo11  7348  omlimcl  7545  omxpenlem  7946  fodomr  7996  fodomfib  8125  r1val1  8532  alephval3  8816  dfac5lem4  8832  dfac5  8834  axdc4lem  9160  fodomb  9229  distrlem1pr  9726  map2psrpr  9810  supsrlem  9811  eqle  10018  swrd0  13286  reuccats1lem  13331  repswswrd  13382  cshwidxmod  13400  rtrclind  13653  sumz  14300  prod1  14513  divalglem8  14961  flodddiv4  14975  pospo  16796  mgm2nsgrplem2  17229  lsmcv  18962  opsrtoslem1  19305  psrbagfsupp  19330  madugsum  20268  hauscmplem  21019  bwth  21023  ptbasfi  21194  hmphindis  21410  fbncp  21453  fgcl  21492  fixufil  21536  uffixfr  21537  mbfima  23205  mbfimaicc  23206  ig1pdvds  23740  zabsle1  24821  tgldimor  25197  ax5seglem4  25612  axcontlem2  25645  axcontlem4  25647  uhgraun  25840  usgfiregdegfi  26438  eupai  26494  usgreghash2spot  26596  numclwwlkun  26606  spansncvi  27895  eigposi  28079  pjnormssi  28411  sumdmdlem  28661  rhmdvdsr  29149  bnj168  30052  bnj521  30059  bnj964  30267  bnj966  30268  bnj1398  30356  cgrdegen  31281  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn1lem14  31377  bj-elid3  32264  bj-ccinftydisj  32277  phpreu  32563  fin2so  32566  matunitlindflem2  32576  poimirlem26  32605  poimirlem28  32607  dvasin  32666  isbnd2  32752  atcvrj0  33732  paddasslem5  34128  pm13.13a  37630  iotavalb  37653  suctrALTcf  38180  suctrALTcfVD  38181  suctrALT3  38182  unisnALT  38184  2sb5ndALT  38190  xreqle  38475  fourierdlem40  39040  fourierdlem78  39077  2ffzoeq  40361  nbgrval  40560  cusgrfi  40674  fusgrregdegfi  40769  rusgr1vtxlem  40787  ifpprsnss  40845  1wlkiswwlksupgr2  41074  elwwlks2ons3  41159  eucrctshift  41411  fusgreghash2wsp  41502  av-numclwlk1lem2f1  41524  difmodm1lt  42111  nn0sumshdiglemA  42211
  Copyright terms: Public domain W3C validator