Theorem biimpa 500

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

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpa	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 218	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 444	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simprbda  651  simplbda  652  pm5.1  898  bimsc1  976  biimp3a  1424  equsex  2281  euor  2500  euan  2518  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  ceqsex  3214  sbciegft  3433  sbeqalb  3455  syl5sseq  3616  elpwunsn  4171  ralxfr2d  4808  propeqop  4895  euotd  4900  relop  5194  elsnxp  5594  sspred  5605  fnbr  5907  f1o00  6083  foelrni  6154  dffv2  6181  iinpreima  6253  funressn  6331  fnex  6386  f1prex  6439  weniso  6504  f1ocnv2d  6784  ofrval  6805  limsssuc  6942  resiexg  6994  eloprabi  7121  1stconst  7152  2ndconst  7153  frxp  7174  poxp  7176  smodm2  7339  smoiso  7346  tz7.44lem1  7388  oev2  7490  oesuclem  7492  oecl  7504  omordi  7533  omwordri  7539  omword2  7541  omordlim  7544  omlimcl  7545  omeulem2  7550  oeordi  7554  oewordri  7559  oelim2  7562  oeoa  7564  oeoe  7566  nnawordi  7588  nnaordex  7605  erth  7678  iiner  7706  pw2f1olem  7949  pw2f1o  7950  onomeneq  8035  onfin2  8037  unxpdomlem2  8050  isinf  8058  findcard2  8085  fipreima  8155  fipwss  8218  cantnfp1lem3  8460  carden2b  8676  carddomi2  8679  infxpenlem  8719  acni2  8752  numacn  8755  alephfp  8814  pwsdompw  8909  ackbij2lem3  8946  cfeq0  8961  cfsuc  8962  cfsmolem  8975  domfin4  9016  axdc3lem2  9156  axdc3lem4  9158  alephreg  9283  fpwwe2  9344  winainflem  9394  r1limwun  9437  inar1  9476  grudomon  9518  nlt1pi  9607  indpi  9608  nqereu  9630  ltbtwnnq  9679  prlem934  9734  prlem936  9748  addgt0sr  9804  leltne  10006  ne0gt0  10021  mullt0  10426  msqgt0  10427  mulne0  10548  divne0  10576  div2neg  10627  ltmul12a  10758  recgt1i  10799  negfi  10850  nn2ge  10922  div4p1lem1div2  11164  nn0lt2  11317  peano5uzi  11342  eluzp1m1  11587  eluzaddi  11590  eluzsubi  11591  uz2m1nn  11639  nn01to3  11657  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  rphalflt  11736  xrleltne  11854  max0sub  11901  xmulpnf1n  11980  xmulge0  11986  xadddi  11997  supxr  12015  supxr2  12016  ixxdisj  12061  ixxun  12062  ixxub  12067  ixxlb  12068  iccgelb  12101  icodisj  12168  difreicc  12175  iccf1o  12187  fzsuc2  12268  fzonmapblen  12381  elfznelfzo  12439  flge0nn0  12483  flge1nn  12484  2submod  12593  modfzo0difsn  12604  seqf1olem2  12703  expubnd  12783  sqlecan  12833  bernneq  12852  bernneq2  12853  expnbnd  12855  discr1  12862  facwordi  12938  faclbnd4lem4  12945  bcpasc  12970  hashgt0n0  13017  elprchashprn2  13045  hash1to3  13128  iswrdi  13164  ffz0iswrd  13187  ccatsymb  13219  ccatass  13224  swrdlend  13283  swrdfv2  13298  swrdspsleq  13301  swrdswrdlem  13311  swrdswrd  13312  swrdswrd0  13314  swrdccatin12lem2b  13337  revccat  13366  revrev  13367  repswccat  13383  2cshw  13410  cshwcsh2id  13425  revco  13431  cshco  13433  s2f1o  13511  s4f1o  13513  wrdlen2i  13534  wwlktovf  13547  ofccat  13556  trclub  13587  sqr0lem  13829  sqrlem2  13832  sqrlem7  13837  max0add  13898  recval  13910  nnabscl  13913  absmax  13917  sqreulem  13947  climi0  14091  lo1bdd2  14103  rlimresb  14144  lo1eq  14147  rlimeq  14148  isercolllem3  14245  climsup  14248  fsumsplit  14318  fsumcom2  14347  fsumcom2OLD  14348  explecnv  14436  fprodser  14518  fprodsplit  14535  fprodcom2  14553  fprodcom2OLD  14554  eftlub  14678  sin02gt0  14761  rpnnen2lem10  14791  dvdsleabs2  14872  mulmoddvds  14889  odd2np1  14903  oexpneg  14907  sqoddm1div8z  14916  bitsf1  15006  sadcaddlem  15017  bitsuz  15034  rplpwr  15114  rppwr  15115  nn0seqcvgd  15121  lcmneg  15154  qredeq  15209  dvdsnprmd  15241  oddprmge3  15250  isprm7  15258  qgt0numnn  15297  phibndlem  15313  hashgcdeq  15332  reumodprminv  15347  coprimeprodsq2  15352  pythagtrip  15377  dvdsprmpweqle  15428  fldivp1  15439  unbenlem  15450  4sqlem9  15488  4sqlem15  15501  4sqlem16  15502  vdwlem6  15528  vdwlem10  15532  vdwlem11  15533  vdwlem13  15535  vdw  15536  prmgaplem7  15599  prmgaplem8  15600  cshwshashlem1  15640  mreuni  16083  cidpropd  16193  subsubc  16336  ffthiso  16412  fuciso  16458  setcmon  16560  setcepi  16561  catciso  16580  funcestrcsetclem7  16609  funcestrcsetclem8  16610  setc1strwun  16616  funcsetcestrclem7  16624  hofcl  16722  hofpropd  16730  yonedalem4c  16740  yonedainv  16744  issstrmgm  17075  imasmnd  17151  pwsco1mhm  17193  imasgrp  17354  subginv  17424  subgmulg  17431  eqger  17467  subgga  17556  orbstafun  17567  orbsta  17569  symggrp  17643  psgnsn  17763  dfod2  17804  gexval  17816  gex1  17829  sylow2blem1  17858  sylow3lem1  17865  pj1eu  17932  efgredlema  17976  frgp0  17996  frgpmhm  18001  odadd1  18074  0cyg  18117  gsumzres  18133  gsumzsplit  18150  gsummptfzcl  18191  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2  18268  dprdsplit  18270  pgpfaclem3  18305  ablfac2  18311  imasring  18442  rhmf1o  18555  kerf1hrm  18566  subrg1  18613  abvneg  18657  lmhmf1o  18867  lmhmima  18868  reslmhm2b  18875  pwssplit0  18879  pwssplit1  18880  lsmspsn  18905  lspdisj  18946  lidlmcl  19038  isnzr2hash  19085  fidomndrnglem  19127  mplsubglem  19255  mplmonmul  19285  mplbas2  19291  subrgascl  19319  subrgasclcl  19320  evlsval2  19341  mpfind  19357  lply1binomsc  19498  absabv  19622  f1lindf  19980  mat0dimscm  20094  scmataddcl  20141  scmatsubcl  20142  smatvscl  20149  mdetunilem8  20244  chfacfscmul0  20482  chfacfscmulfsupp  20483  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulfsupp  20487  chfacfpmmulgsum  20488  cpmidpmatlem3  20496  chcoeffeqlem  20509  cayleyhamilton0  20513  cayleyhamiltonALT  20515  cayleyhamilton1  20516  elcls  20687  clsndisj  20689  isclo2  20702  neiuni  20736  neissex  20741  neiptopreu  20747  tgrest  20773  neitr  20794  tgcnp  20867  lmfpm  20909  lmcl  20911  lmss  20912  lmff  20915  ist1-2  20961  cnt1  20964  cmpsublem  21012  clscon  21043  locfindis  21143  kgeni  21150  kgenidm  21160  txcnpi  21221  ptpjopn  21225  ptclsg  21228  txcmplem1  21254  qtoptop2  21312  qtoptopon  21317  r0sep  21361  ptunhmeo  21421  t0kq  21431  fsubbas  21481  neifil  21494  uffixsn  21539  ufildr  21545  rnelfm  21567  isfcls2  21627  uffclsflim  21645  alexsublem  21658  cnextfun  21678  cnextfvval  21679  cnextf  21680  cnextcn  21681  tmdcn2  21703  symgtgp  21715  tsmssplit  21765  ustuni  21840  trust  21843  utoptop  21848  restutop  21851  restutopopn  21852  ustuqtop1  21855  ustuqtop2  21856  ustuqtop3  21857  ustuqtop4  21858  utop2nei  21864  utop3cls  21865  ucncn  21899  trcfilu  21908  cfiluweak  21909  psmetdmdm  21920  xmeter  22048  prdsbl  22106  neibl  22116  methaus  22135  prdsxmslem2  22144  metustto  22168  metustexhalf  22171  metust  22173  cfilucfil  22174  psmetutop  22182  tngngp2  22266  tngngp  22268  tgqioo  22411  xrsxmet  22420  icccmplem1  22433  icccmplem2  22434  cnmpt2pc  22535  iihalf2  22540  icoopnst  22546  iocopnst  22547  xrhmeo  22553  lebnumlem1  22568  lebnumlem3  22570  pi1blem  22647  pi1grplem  22657  pi1xfrf  22661  pi1xfr  22663  pi1xfrcnvlem  22664  pi1cof  22667  pi1coghm  22669  cmetcaulem  22894  causs  22904  metcld  22912  lmcau  22919  rrxcph  22988  minveclem4  23011  ivthlem2  23028  ivthlem3  23029  ivthicc  23034  ovolshftlem1  23084  ovolicc1  23091  ovolicopnf  23099  volfiniun  23122  uniioombllem3  23159  dyaddisjlem  23169  vitalilem2  23184  itg1ge0  23259  mbfi1fseqlem3  23290  xrge0f  23304  itg2seq  23315  itg2monolem1  23323  itg2addlem  23331  itg2gt0  23333  iblcnlem  23361  itgss3  23387  itgsplit  23408  dvnff  23492  dvferm2  23554  dvlip2  23562  dveq0  23567  dvge0  23573  dvcnvre  23586  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  ftc1lem2  23603  ftc1lem4  23606  ftc1lem5  23607  ftc1cn  23610  ftc2  23611  itgsubstlem  23615  coe1mul3  23663  ply1divex  23700  dgrlem  23789  dgrlb  23796  coemulhi  23814  dgrlt  23826  dgrmul  23830  plydivlem4  23855  fta1  23867  aaliou2b  23900  taylplem2  23922  dvtaylp  23928  ulmcau  23953  tanabsge  24062  sinq12gt0  24063  argimgt0  24162  cxplea  24242  cxple2  24243  cxpsqrt  24249  cxpaddlelem  24292  loglesqrt  24299  logrec  24301  ang180lem2  24340  lawcos  24346  asinlem3a  24397  asinlem3  24398  asinsin  24419  atanlogaddlem  24440  atanlogadd  24441  atanlogsub  24443  atantan  24450  atanbnd  24453  atantayl2  24465  efrlim  24496  wilthlem2  24595  basellem2  24608  sqfpc  24663  ppieq0  24702  sqff1o  24708  fsumdvdscom  24711  ppiub  24729  chpeq0  24733  chtleppi  24735  fsumvma  24738  fsumvma2  24739  mersenne  24752  dchrabs2  24787  dchr1re  24788  dchrpt  24792  lgsdilem  24849  lgsdinn0  24870  gausslemma2dlem0b  24882  gausslemma2dlem1a  24890  gausslemma2dlem5  24896  gausslemma2dlem6  24897  lgsquad3  24912  m1lgs  24913  2lgslem1a  24916  2lgslem1  24919  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  2sqlem6  24948  rpvmasumlem  24976  dchrisumlem3  24980  dchrisum0flblem1  24997  pntibndlem2a  25079  pntlem3  25098  padicabv  25119  ercgrg  25212  tglnunirn  25243  tglineeltr  25326  mirln2  25372  mirbtwnhl  25375  isperp2  25410  outpasch  25447  lnopp2hpgb  25455  ttgbtwnid  25564  axcontlem2  25645  axcontlem12  25655  usgra1  25902  edgprvtx  25914  usgraedg4  25916  nbgraop  25952  nbgracnvfv  25969  nbcusgra  25992  wlkdvspthlem  26137  fargshiftf1  26165  fargshiftfo  26166  wlkiswwlk1  26218  clwlkisclwwlklem2a4  26312  clwlkisclwwlk2  26318  clwwlkf1  26324  clwwnisshclwwn  26337  eleclclwwlknlem2  26346  erclwwlkneqlen  26352  clwlkfclwwlk2wrd  26367  clwlkf1clwwlklem3  26375  clwlkf1clwwlklem  26376  usg2spthonot  26415  eupatrl  26495  eupap1  26503  frgrancvvdeqlemA  26564  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgrawopreglem4  26574  numclwwlkovf2ex  26613  numclwwlk2lem1  26629  frgrareggt1  26643  frgraregord013  26645  cnnv  26916  nmounbseqi  27016  nmounbseqiALT  27017  nmlnogt0  27036  nmblolbii  27038  blocnilem  27043  ajmoi  27098  minvecolem4  27120  hhnv  27406  norm1  27490  hhssnv  27505  pjhtheu  27637  pjpreeq  27641  spanunsni  27822  fh1  27861  fh2  27862  cm2j  27863  chscllem4  27883  pjid  27938  adjmo  28075  eleigveccl  28202  eigvalcl  28204  eigvec1  28205  eighmre  28206  eighmorth  28207  nmop0h  28234  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  lncnopbd  28280  nmbdfnlbi  28292  nmcfnlbi  28295  cnlnadjeui  28320  branmfn  28348  rnbra  28350  nmopleid  28382  strlem5  28498  hstrlem5  28506  dmdbr3  28548  dmdbr4  28549  mdsl3  28559  hatomistici  28605  cvexchlem  28611  chirredlem1  28633  chirredlem2  28634  chirredi  28637  atcvat3i  28639  atcvat4i  28640  atabsi  28644  mdsymlem1  28646  mdsymlem3  28648  mdsymlem5  28650  dmdbr5ati  28665  cdj1i  28676  foresf1o  28727  rabfodom  28728  elabreximd  28732  elpreq  28744  f1o3d  28813  acunirnmpt2f  28843  disjdsct  28863  1stpreimas  28866  fcobij  28888  fpwrelmapffslem  28895  nn0sqeq1  28901  xrofsup  28923  eliccelico  28929  elicoelioo  28930  numdenneg  28950  xrge0addgt0  29022  xrge0adddir  29023  xrge0npcan  29025  omndmul3  29044  submarchi  29071  archirng  29073  archirngz  29074  archiexdiv  29075  archiabllem1a  29076  1smat1  29198  madjusmdetlem2  29222  locfinreflem  29235  metideq  29264  unitdivcld  29275  cnre2csqlem  29284  ordtconlem1  29298  fmcncfil  29305  lmxrge0  29326  pl1cn  29329  zrhunitpreima  29350  elzdif0  29352  qqhval2lem  29353  qqhf  29358  indf1ofs  29415  esumfsup  29459  esumpcvgval  29467  esum2dlem  29481  esum2d  29482  esumiun  29483  sigasspw  29506  issgon  29513  ispisys2  29543  meascnbl  29609  voliune  29619  volfiniune  29620  omssubaddlem  29688  carsggect  29707  carsgclctunlem2  29708  oddpwdc  29743  eulerpartlems  29749  eulerpartlemgvv  29765  ballotlemfrcn0  29918  sgncl  29927  sgnneg  29929  sgn3da  29930  sgnmul  29931  sgnsub  29933  gsumnunsn  29942  signsplypnf  29953  signsply0  29954  signslema  29965  signstfvneq0  29975  signsvfpn  29988  signsvfnn  29989  bnj563  30067  bnj1001  30282  subfacp1lem5  30420  subfacp1lem6  30421  erdszelem9  30435  ptpcon  30469  rescon  30482  cvmlift3lem7  30561  msrrcl  30694  trpredrec  30982  btwnintr  31296  btwnouttr  31301  cgrxfr  31332  btwnconn1lem12  31375  colinbtwnle  31395  lineelsb2  31425  nn0prpwlem  31487  neibastop3  31527  onintopsscon  31609  bj-restsnss  32217  bj-restsnss2  32218  taupilem1  32344  relowlssretop  32387  finxpsuclem  32410  unccur  32562  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem2  32581  poimirlem8  32587  poimirlem14  32593  poimirlem15  32594  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  heicant  32614  mblfinlem2  32617  itg2gt0cn  32635  itgaddnclem2  32639  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem2  32656  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anc  32663  ftc2nc  32664  dvasin  32666  areacirclem5  32674  areacirc  32675  fdc  32711  incsequz  32714  blbnd  32756  prdstotbnd  32763  cnpwstotbnd  32766  ismtyres  32777  rngohomf  32935  rngohom1  32937  rngohomadd  32938  rngohommul  32939  idlss  32985  idl0cl  32987  idladdcl  32988  idllmulcl  32989  idlrmulcl  32990  maxidlnr  33011  maxidlmax  33012  smprngopr  33021  pridlc  33040  ac6s6f  33151  lshpnel2N  33290  islsati  33299  lkr0f  33399  lfl1dim  33426  lfl1dim2N  33427  omlfh1N  33563  leat  33598  atlatmstc  33624  cvlatexch3  33643  lnnat  33731  cvrat3  33746  cvrat4  33747  3dim3  33773  dalem4  33969  dalem39  34015  paddasslem12  34135  psubcliN  34242  pmapojoinN  34272  lhpm0atN  34333  lhprelat3N  34344  trlnid  34484  trlval3  34492  cdleme22b  34647  trljco  35046  diaglbN  35362  dibvalrel  35470  dicvalrelN  35492  diclspsn  35501  dih1dimatlem  35636  dihlatat  35644  lcfl6  35807  lcfl8  35809  lcfrvalsnN  35848  lcfrlem9  35857  mapdheq2  36036  hlhillcs  36268  hlhilhillem  36270  mzpindd  36327  lzunuz  36349  2rexfrabdioph  36378  irrapxlem3  36406  pellexlem2  36412  pellexlem5  36415  pell1234qrreccl  36436  pell14qrdich  36451  pell1qrge1  36452  elpell1qr2  36454  reglogltb  36473  reglogleb  36474  rmxycomplete  36500  2nn0ind  36528  congabseq  36559  acongrep  36565  acongeq  36568  jm2.22  36580  jm2.26lem3  36586  pw2f1ocnv  36622  limsuc2  36629  fnwe2lem3  36640  aomclem6  36647  kercvrlsm  36671  pwssplit4  36677  lpirlnr  36706  rfovcnvf1od  37318  dssmapnvod  37334  cvgdvgrat  37534  radcnvrat  37535  dvconstbi  37555  bccbc  37566  bi2imp  37709  ax6e2ndeqALT  38189  mulltgt0  38204  refsumcn  38212  cncmpmax  38214  mapdm0  38378  unirnmapsn  38401  icoiccdif  38597  climinf  38673  climreeq  38680  climeldmeq  38732  coskpi2  38749  cosknegpi  38752  icccncfext  38773  dvmptfprodlem  38834  volioore  38883  stoweidlem27  38920  stoweidlem29  38922  stoweidlem31  38924  stoweidlem34  38927  stoweidlem48  38941  stoweidlem59  38952  fourierdlem109  39108  fourierswlem  39123  elaa2  39127  etransclem37  39164  hspmbllem2  39517  sigarcol  39702  reuan  39829  ndmaovg  39913  iccelpart  39971  fmtno4prmfac  40022  2pwp1prmfmtno  40042  sfprmdvdsmersenne  40058  lighneallem3  40062  proththd  40069  evenm1odd  40090  evenp1odd  40091  nnoALTV  40144  stgoldbwt  40198  bgoldbst  40200  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem2  40222  pfxeq  40267  pfxccatin12lem1  40286  repswpfx  40299  riotaeqimp  40338  subsubelfzo0  40359  fusgrfisstep  40548  nbupgrres  40592  usgrnbcnvfv  40593  nbusgredgeu  40594  nbcplgr  40656  cusgrexi  40662  cusgrsizeinds  40668  uhgr0edg0rgr  40773  1wlkl1loop  40842  upgr1wlkwlk  40847  usgr2pthlem  40969  wspthnp  41048  elwwlks2ons3  41159  elwspths2on  41163  usgr2wspthons3  41167  clwlkclwwlklem2a4  41206  clwlkclwwlk2  41212  clwwlksn1loop  41216  clwwlksf1  41224  clwwisshclwws  41235  eleclclwwlksnlem2  41246  clwlksfclwwlk2wrd  41265  clwlksf1clwwlklem3  41274  clwlksf1clwwlklem  41275  1pthon2v-av  41320  upgr3v3e3cycl  41347  eupth2lemb  41405  frgrncvvdeqlemA  41476  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  frgrwopreglem4  41484  av-numclwwlkovf2ex  41517  av-numclwwlk2lem1  41532  av-frgrareggt1  41547  av-frgraregord013  41549  rnghmf1o  41693  rnghmsubcsetclem1  41767  zrinitorngc  41792  zrtermorngc  41793  rhmsubcsetclem1  41813  rhmsubcrngclem1  41819  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  zrtermoringc  41862  ply1sclrmsm  41965  lincfsuppcl  41996  zofldiv2  42119  elbigolo1  42149  blennn0em1  42183  blennn0e2  42186  dig2nn0ld  42196  nn0sumshdiglem2  42214