Theorem biimpac 486

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1

Assertion

Ref	Expression
biimpac

Proof of Theorem biimpac

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3
2	1	biimpcd 224	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  gencbvex2  3154  2reu5  3308  ordnbtwn  4973  poltletr  5407  tz6.12-1  5887  nfunsn  5902  onsucuni2  6669  smo11  7054  omlimcl  7246  omxpenlem  7638  fodomr  7688  fodomfib  7820  r1val1  8225  alephval3  8512  dfac5lem4  8528  dfac5  8530  axdc4lem  8856  fodomb  8925  distrlem1pr  9424  map2psrpr  9508  supsrlem  9509  eqle  9708  snopiswrd  12556  swrd0  12658  reuccats1lem  12705  repswswrd  12756  cshwidxmod  12774  sumz  13544  prod1  13751  divalglem8  14058  pospo  15603  mgm2nsgrplem2  16037  lsmcv  17787  opsrtoslem1  18148  psrbagfsupp  18175  psrbagsuppfiOLD  18176  madugsum  19145  hauscmplem  19906  bwth  19910  ptbasfi  20082  hmphindis  20298  fbncp  20340  fgcl  20379  fixufil  20423  uffixfr  20424  mbfima  22039  mbfimaicc  22040  ig1pdvds  22577  tgldimor  23893  ax5seglem4  24235  axcontlem2  24268  axcontlem4  24270  uhgraun  24311  usgfiregdegfi  24911  eupai  24967  usgreghash2spot  25069  spansncvi  26570  eigposi  26755  pjnormssi  27087  sumdmdlem  27337  rhmdvdsr  27808  rtrclind  29072  cgrdegen  29654  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem14  29750  fin2so  30040  dvasin  30103  isbnd2  30279  pm13.13a  31314  iotavalb  31337  fourierdlem40  31929  fourierdlem78  31967  2ffzoeq  32341  uhgun  32380  biimpa21  33342  suctrALTcf  33722  suctrALTcfVD  33723  suctrALT3  33724  unisnALT  33726  bnj168  33785  bnj521  33792  bnj964  34001  bnj966  34002  bnj1398  34090  bj-elid3  34601  bj-ccinftydisj  34616  atcvrj0  35152  paddasslem5  35548

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 185  df-an 371