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

Theorem biimpac 482
 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 252 . 2 (𝜓 → (𝜑𝜒))
32imp 410 1 ((𝜓𝜑) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  gencbvex2  3525  2reu5  3724  ifpprsnss  4674  poltletr  5970  ordnbtwn  6259  tz6.12-1  6674  funopsn  6892  onsucuni2  7534  1stconst  7782  2ndconst  7783  smo11  7988  omlimcl  8191  omxpenlem  8605  fodomr  8656  fodomfib  8786  infsupprpr  8956  r1val1  9203  alephval3  9525  dfac5lem4  9541  dfac5  9543  axdc4lem  9866  fodomb  9937  distrlem1pr  10436  map2psrpr  10521  supsrlem  10522  eqle  10731  swrd0  14011  repswswrd  14137  cshwidxmod  14156  rtrclind  14415  sumz  15070  prod1  15289  divalglem8  15740  flodddiv4  15753  pospo  17574  mgm2nsgrplem2  18075  lsmcv  19904  opsrtoslem1  20721  psrbagfsupp  20746  madugsum  21246  hauscmplem  22009  bwth  22013  ptbasfi  22184  hmphindis  22400  fbncp  22442  fgcl  22481  fixufil  22525  uffixfr  22526  mbfima  24232  mbfimaicc  24233  ig1pdvds  24775  zabsle1  25878  tgldimor  26294  ax5seglem4  26724  axcontlem2  26757  axcontlem4  26759  nbgrval  27124  cusgrfi  27246  fusgrregdegfi  27357  rusgr1vtxlem  27375  wlkiswwlksupgr2  27661  elwwlks2ons3  27739  clwwlknonwwlknonb  27889  eucrctshift  28026  spansncvi  29433  eigposi  29617  pjnormssi  29949  sumdmdlem  30199  rhmdvdsr  30923  sraring  31044  tngdim  31068  bnj168  32074  bnj521  32081  bnj964  32289  bnj966  32290  bnj1398  32380  lfuhgr3  32440  acycgrislfgr  32473  cgrdegen  33539  btwnconn1lem11  33632  btwnconn1lem12  33633  btwnconn1lem14  33635  bj-opelidb1  34529  bj-inexeqex  34530  bj-idreseqb  34539  bj-ideqg1ALT  34541  bj-ccinftydisj  34589  phpreu  34999  fin2so  35002  matunitlindflem2  35012  poimirlem26  35041  poimirlem28  35043  dvasin  35099  isbnd2  35179  atcvrj0  36682  paddasslem5  37078  pm13.13a  41045  iotavalb  41068  suctrALTcf  41562  suctrALTcfVD  41563  suctrALT3  41564  unisnALT  41566  2sb5ndALT  41572  xreqle  41889  supminfxr2  42047  fourierdlem40  42728  fourierdlem78  42765  tz6.12-afv2  43735  afv2fv0  43760  2ffzoeq  43824  uspgropssxp  44311  uspgrsprfo  44315  difmodm1lt  44875  nn0sumshdiglemA  44972  itscnhlc0yqe  45112
 Copyright terms: Public domain W3C validator