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

Theorem biimpac 480
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 249 . 2 (𝜓 → (𝜑𝜒))
32imp 408 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  r19.29r  3118  gencbvex2  3504  2reu5  3715  ifpprsnss  4724  dfiun2g  4989  poltletr  6083  ordnbtwn  6407  tz6.12-1OLD  6862  funopsn  7089  onsucuni2  7760  1stconst  8021  2ndconst  8022  smo11  8278  omlimcl  8493  omxpenlem  8951  fodomr  9006  f1oenfirn  9061  f1domfi  9062  fodomfib  9204  infsupprpr  9374  r1val1  9656  alephval3  9980  dfac5lem4  9996  dfac5  9998  axdc4lem  10325  fodomb  10396  distrlem1pr  10895  map2psrpr  10980  supsrlem  10981  eqle  11191  swrd0  14478  repswswrd  14604  cshwidxmod  14623  rtrclind  14884  sumz  15542  prod1  15762  divalglem8  16217  flodddiv4  16230  pospo  18169  mgm2nsgrplem2  18664  rhmdvdsr  20105  lsmcv  20526  psrbagfsuppOLD  21247  opsrtoslem1  21385  madugsum  21915  hauscmplem  22680  bwth  22684  ptbasfi  22855  hmphindis  23071  fbncp  23113  fgcl  23152  fixufil  23196  uffixfr  23197  mbfima  24917  mbfimaicc  24918  ig1pdvds  25464  zabsle1  26567  tgldimor  27243  ax5seglem4  27680  axcontlem2  27713  axcontlem4  27715  nbgrval  28083  cusgrfi  28205  fusgrregdegfi  28316  rusgr1vtxlem  28334  wlkiswwlksupgr2  28621  elwwlks2ons3  28699  clwwlknonwwlknonb  28849  eucrctshift  28986  spansncvi  30393  eigposi  30577  pjnormssi  30909  sumdmdlem  31159  sraring  32070  tngdim  32094  bnj168  33116  bnj964  33329  bnj966  33330  bnj1398  33420  fnrelpredd  33467  lfuhgr3  33487  acycgrislfgr  33520  cgrdegen  34485  btwnconn1lem11  34578  btwnconn1lem12  34579  btwnconn1lem14  34581  bj-opelidb1  35520  bj-inexeqex  35521  bj-idreseqb  35530  bj-ideqg1ALT  35532  bj-ccinftydisj  35580  phpreu  35958  fin2so  35961  matunitlindflem2  35971  poimirlem26  36000  poimirlem28  36002  dvasin  36058  isbnd2  36138  atcvrj0  37787  paddasslem5  38183  pm13.13a  42452  iotavalb  42475  suctrALTcf  42969  suctrALTcfVD  42970  suctrALT3  42971  unisnALT  42973  2sb5ndALT  42979  xreqle  43311  supminfxr2  43463  fourierdlem40  44143  fourierdlem78  44180  tz6.12-afv2  45227  afv2fv0  45252  2ffzoeq  45315  uspgropssxp  45801  uspgrsprfo  45805  difmodm1lt  46363  nn0sumshdiglemA  46460  itscnhlc0yqe  46600
  Copyright terms: Public domain W3C validator