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

Theorem biimpac 503
 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 445 1 ((𝜓𝜑) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 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 386 This theorem is referenced by:  gencbvex2  3241  2reu5  3403  ifpprsnss  4276  poltletr  5497  ordnbtwn  5785  ordnbtwnOLD  5786  tz6.12-1  6177  nfunsn  6192  funopsn  6378  onsucuni2  6996  smo11  7421  omlimcl  7618  omxpenlem  8021  fodomr  8071  fodomfib  8200  r1val1  8609  alephval3  8893  dfac5lem4  8909  dfac5  8911  axdc4lem  9237  fodomb  9308  distrlem1pr  9807  map2psrpr  9891  supsrlem  9892  eqle  10099  swrd0  13388  reuccats1lem  13433  repswswrd  13484  cshwidxmod  13502  rtrclind  13755  sumz  14402  prod1  14618  divalglem8  15066  flodddiv4  15080  pospo  16913  mgm2nsgrplem2  17346  lsmcv  19081  opsrtoslem1  19424  psrbagfsupp  19449  madugsum  20389  hauscmplem  21149  bwth  21153  ptbasfi  21324  hmphindis  21540  fbncp  21583  fgcl  21622  fixufil  21666  uffixfr  21667  mbfima  23339  mbfimaicc  23340  ig1pdvds  23874  zabsle1  24955  tgldimor  25331  ax5seglem4  25746  axcontlem2  25779  axcontlem4  25781  nbgrval  26155  cusgrfi  26275  fusgrregdegfi  26369  rusgr1vtxlem  26387  wlkiswwlksupgr2  26666  elwwlks2ons3  26751  eucrctshift  27003  fusgreghash2wsp  27094  numclwlk1lem2f1  27116  spansncvi  28399  eigposi  28583  pjnormssi  28915  sumdmdlem  29165  rhmdvdsr  29645  bnj168  30559  bnj521  30566  bnj964  30774  bnj966  30775  bnj1398  30863  cgrdegen  31806  btwnconn1lem11  31899  btwnconn1lem12  31900  btwnconn1lem14  31902  bj-elid3  32759  bj-ccinftydisj  32772  phpreu  33064  fin2so  33067  matunitlindflem2  33077  poimirlem26  33106  poimirlem28  33108  dvasin  33167  isbnd2  33253  atcvrj0  34233  paddasslem5  34629  pm13.13a  38129  iotavalb  38152  suctrALTcf  38680  suctrALTcfVD  38681  suctrALT3  38682  unisnALT  38684  2sb5ndALT  38690  xreqle  39033  fourierdlem40  39701  fourierdlem78  39738  2ffzoeq  40665  uspgropssxp  41070  uspgrsprfo  41074  difmodm1lt  41635  nn0sumshdiglemA  41735
 Copyright terms: Public domain W3C validator