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

Theorem biimpac 479
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 250 . 2 (𝜓 → (𝜑𝜒))
32imp 407 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  gencbvex2  3548  2reu5  3746  ifpprsnss  4692  poltletr  5985  ordnbtwn  6274  tz6.12-1  6685  funopsn  6902  onsucuni2  7538  1stconst  7784  2ndconst  7785  smo11  7990  omlimcl  8193  omxpenlem  8606  fodomr  8656  fodomfib  8786  infsupprpr  8956  r1val1  9203  alephval3  9524  dfac5lem4  9540  dfac5  9542  axdc4lem  9865  fodomb  9936  distrlem1pr  10435  map2psrpr  10520  supsrlem  10521  eqle  10730  swrd0  14008  repswswrd  14134  cshwidxmod  14153  rtrclind  14412  sumz  15067  prod1  15286  divalglem8  15739  flodddiv4  15752  pospo  17571  mgm2nsgrplem2  18022  lsmcv  19842  opsrtoslem1  20192  psrbagfsupp  20217  madugsum  21180  hauscmplem  21942  bwth  21946  ptbasfi  22117  hmphindis  22333  fbncp  22375  fgcl  22414  fixufil  22458  uffixfr  22459  mbfima  24158  mbfimaicc  24159  ig1pdvds  24697  zabsle1  25799  tgldimor  26215  ax5seglem4  26645  axcontlem2  26678  axcontlem4  26680  nbgrval  27045  cusgrfi  27167  fusgrregdegfi  27278  rusgr1vtxlem  27296  wlkiswwlksupgr2  27582  elwwlks2ons3  27661  clwwlknonwwlknonb  27812  eucrctshift  27949  spansncvi  29356  eigposi  29540  pjnormssi  29872  sumdmdlem  30122  rhmdvdsr  30818  sraring  30886  tngdim  30910  bnj168  31899  bnj521  31906  bnj964  32114  bnj966  32115  bnj1398  32203  lfuhgr3  32263  acycgrislfgr  32296  cgrdegen  33362  btwnconn1lem11  33455  btwnconn1lem12  33456  btwnconn1lem14  33458  bj-opelidb1  34337  bj-inexeqex  34338  bj-idreseqb  34347  bj-ideqg1ALT  34349  bj-ccinftydisj  34387  phpreu  34757  fin2so  34760  matunitlindflem2  34770  poimirlem26  34799  poimirlem28  34801  dvasin  34859  isbnd2  34942  atcvrj0  36444  paddasslem5  36840  pm13.13a  40616  iotavalb  40639  suctrALTcf  41133  suctrALTcfVD  41134  suctrALT3  41135  unisnALT  41137  2sb5ndALT  41143  xreqle  41462  supminfxr2  41621  fourierdlem40  42309  fourierdlem78  42346  tz6.12-afv2  43316  afv2fv0  43341  2ffzoeq  43405  uspgropssxp  43896  uspgrsprfo  43900  difmodm1lt  44510  nn0sumshdiglemA  44607  itscnhlc0yqe  44674
  Copyright terms: Public domain W3C validator