Theorem biimpa 477

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 230	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 407	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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:  simprbda  499  simplbda  500  pm5.1  821  biimp3a  1461  equsex  2396  euor  2662  euorv  2663  euan  2674  euanv  2678  cgsexg  3480  cgsex2g  3481  cgsex4g  3482  ceqsex  3483  sbciegft  3740  sbeqalb  3768  reuan  3812  sseqtrid  3944  elpwunsn  4532  ralxfr2d  5207  propeqop  5293  euotd  5299  relop  5612  elsnxp  6022  sspred  6036  fnbr  6334  f1o00  6522  nfunsn  6580  foelrni  6600  dffv2  6628  iinpreima  6707  funressn  6789  fnex  6851  f1prex  6910  weniso  6975  riotaeqimp  7005  f1ocnv2d  7261  ofrval  7282  limsssuc  7426  opreuopreu  7595  eloprabi  7622  frxp  7678  poxp  7680  smodm2  7849  smoiso  7856  tz7.44lem1  7898  oev2  8004  oesuclem  8006  oecl  8018  omordi  8047  omwordri  8053  omword2  8055  omordlim  8058  omlimcl  8059  omeulem2  8064  oeordi  8068  oewordri  8073  oelim2  8076  oeoa  8078  oeoe  8080  nnawordi  8102  nnaordex  8119  erth  8193  iiner  8224  pw2f1olem  8473  pw2f1o  8474  onomeneq  8559  onfin2  8561  unxpdomlem2  8574  isinf  8582  findcard2  8609  fipreima  8681  fipwss  8744  preleqALT  8931  cantnfp1lem3  8994  carden2b  9247  carddomi2  9250  infxpenlem  9290  acni2  9323  numacn  9326  alephfp  9385  pwsdompw  9477  ackbij2lem3  9514  cfeq0  9529  cfsuc  9530  cfsmolem  9543  domfin4  9584  axdc3lem2  9724  axdc3lem4  9726  alephreg  9855  fpwwe2  9916  winainflem  9966  r1limwun  10009  inar1  10048  grudomon  10090  nlt1pi  10179  indpi  10180  nqereu  10202  ltbtwnnq  10251  prlem934  10306  prlem936  10320  addgt0sr  10377  leltne  10582  ne0gt0  10597  mullt0  11012  msqgt0  11013  mulne0  11135  divne0  11163  div2neg  11216  ltmul12a  11349  recgt1i  11390  negfi  11442  div4p1lem1div2  11745  nn0lt2  11899  peano5uzi  11925  eluzp1m1  12122  eluzaddi  12125  eluzsubi  12126  uz2m1nn  12177  nn01to3  12195  rpnnen1lem5  12235  rphalflt  12273  xrleltne  12393  max0sub  12444  xmulpnf1n  12526  xmulge0  12532  xadddi  12543  supxr  12561  supxr2  12562  ixxdisj  12608  ixxun  12609  ixxub  12614  ixxlb  12615  iccgelb  12648  icodisj  12717  difreicc  12725  iccf1o  12737  fzsuc2  12820  fzonmapblen  12938  elfznelfzo  12997  flge0nn0  13045  flge1nn  13046  2submod  13155  modfzo0difsn  13166  seqf1olem2  13265  expubnd  13396  sqlecan  13426  bernneq  13445  bernneq2  13446  expnbnd  13448  discr1  13455  facwordi  13504  faclbnd4lem4  13511  bcpasc  13536  hashgt0n0  13581  elprchashprn2  13610  hash1to3  13700  iswrdi  13716  ffz0iswrdOLD  13743  ccatsymb  13785  ccatass  13791  swrdlend  13856  swrdfv2  13864  swrdspsleq  13868  pfxeq  13899  swrdswrdlem  13907  swrdswrd  13908  swrdpfx  13910  pfxccatin12lem1  13931  revccat  13969  revrev  13970  repswpfx  13988  repswccat  13989  2cshw  14016  cshwcsh2id  14031  revco  14037  cshco  14039  s2f1o  14119  s4f1o  14121  wrdlen2i  14145  wwlktovf  14159  ofccat  14168  trclub  14197  sqr0lem  14439  sqrlem2  14442  sqrlem7  14447  max0add  14509  recval  14521  nnabscl  14524  absmax  14528  sqreulem  14558  climi0  14708  lo1bdd2  14720  rlimresb  14761  lo1eq  14764  rlimeq  14765  isercolllem3  14862  climsup  14865  fsumsplit  14935  fsumcom2  14967  explecnv  15058  fprodser  15141  fprodsplit  15158  fprodcom2  15176  eftlub  15300  sin02gt0  15383  rpnnen2lem10  15414  dvdsleabs2  15500  odd2np1  15528  oexpneg  15532  sqoddm1div8z  15541  bitsf1  15633  sadcaddlem  15644  bitsuz  15661  rplpwr  15741  rppwr  15742  nn0seqcvgd  15748  lcmneg  15781  qredeq  15835  dvdsnprmd  15868  oddprmge3  15878  ge2nprmge4  15879  isprm7  15886  qgt0numnn  15925  phibndlem  15941  hashgcdeq  15960  reumodprminv  15975  coprimeprodsq2  15980  pythagtrip  16005  dvdsprmpweqle  16056  fldivp1  16067  unbenlem  16078  4sqlem9  16116  4sqlem15  16129  4sqlem16  16130  vdwlem6  16156  vdwlem10  16160  vdwlem11  16161  vdwlem13  16163  vdw  16164  prmgaplem7  16227  prmgaplem8  16228  cshwshashlem1  16263  mreuni  16705  cidpropd  16814  subsubc  16957  ffthiso  17033  fuciso  17079  setcmon  17181  setcepi  17182  catciso  17201  funcestrcsetclem7  17230  funcestrcsetclem8  17231  setc1strwun  17237  funcsetcestrclem7  17245  hofcl  17343  hofpropd  17351  yonedalem4c  17361  yonedainv  17365  issstrmgm  17696  imasmnd  17772  pwsco1mhm  17814  imasgrp  17977  subginv  18045  subgmulg  18052  eqger  18088  subgga  18176  orbstafun  18187  orbsta  18189  symggrp  18264  psgnsn  18384  dfod2  18426  gexval  18438  gex1  18451  sylow2blem1  18480  sylow3lem1  18487  pj1eu  18554  efgredlema  18598  frgp0  18618  frgpmhm  18623  odadd1  18696  0cyg  18739  gsumzres  18755  gsumzsplit  18772  gsummptfzcl  18814  dprd2dlem1  18885  dprd2da  18886  dmdprdsplit2  18890  dprdsplit  18892  pgpfaclem3  18927  ablfac2  18933  imasring  19064  rhmf1o  19179  kerf1ghm  19192  kerf1hrmOLD  19193  subrg1  19240  abvneg  19300  lmhmf1o  19513  lmhmima  19514  reslmhm2b  19521  pwssplit0  19525  pwssplit1  19526  lsmspsn  19551  lspdisj  19592  lidlmcl  19684  isnzr2hash  19731  fidomndrnglem  19773  mplsubglem  19907  mplmonmul  19937  mplbas2  19943  subrgascl  19970  subrgasclcl  19971  evlsval2  19992  mpfind  20008  lply1binomsc  20163  absabv  20289  phlssphl  20490  f1lindf  20653  mat0dimscm  20767  scmataddcl  20814  scmatsubcl  20815  smatvscl  20822  mdetunilem8  20917  chfacfscmul0  21155  chfacfscmulfsupp  21156  chfacfscmulgsum  21157  chfacfpmmul0  21159  chfacfpmmulfsupp  21160  chfacfpmmulgsum  21161  cpmidpmatlem3  21169  chcoeffeqlem  21182  cayleyhamilton0  21186  cayleyhamiltonALT  21188  cayleyhamilton1  21189  elcls  21370  clsndisj  21372  isclo2  21385  neiuni  21419  neissex  21424  neiptopreu  21430  tgrest  21456  neitr  21477  tgcnp  21550  lmfpm  21592  lmcl  21594  lmss  21595  lmff  21598  ist1-2  21644  cnt1  21647  cmpsublem  21696  clsconn  21727  locfindis  21827  kgeni  21834  kgenidm  21844  txcnpi  21905  ptpjopn  21909  ptclsg  21912  txcmplem1  21938  qtoptop2  21996  qtoptopon  22001  r0sep  22045  ptunhmeo  22105  t0kq  22115  fsubbas  22164  neifil  22177  uffixsn  22222  ufildr  22228  rnelfm  22250  isfcls2  22310  uffclsflim  22328  alexsublem  22341  cnextfun  22361  cnextfvval  22362  cnextf  22363  cnextcn  22364  tmdcn2  22386  symgtgp  22398  tsmssplit  22448  ustuni  22523  trust  22526  utoptop  22531  restutop  22534  restutopopn  22535  ustuqtop1  22538  ustuqtop2  22539  ustuqtop3  22540  ustuqtop4  22541  utop2nei  22547  utop3cls  22548  ucncn  22582  trcfilu  22591  cfiluweak  22592  psmetdmdm  22603  xmeter  22731  prdsbl  22789  neibl  22799  methaus  22818  prdsxmslem2  22827  metustto  22851  metustexhalf  22854  metust  22856  cfilucfil  22857  psmetutop  22865  tngngp2  22949  tngngp  22951  tgqioo  23096  xrsxmet  23105  icccmplem1  23118  icccmplem2  23119  cnmpopc  23220  iihalf2  23225  icoopnst  23231  iocopnst  23232  xrhmeo  23238  lebnumlem1  23253  lebnumlem3  23255  pi1blem  23331  pi1grplem  23341  pi1xfrf  23345  pi1xfr  23347  pi1xfrcnvlem  23348  pi1cof  23351  pi1coghm  23353  cmetcaulem  23579  causs  23589  metcld  23597  lmcau  23604  rrxcph  23683  minveclem4  23723  ivthlem2  23741  ivthlem3  23742  ivthicc  23747  ovolshftlem1  23798  ovolicc1  23805  ovolicopnf  23813  volfiniun  23836  uniioombllem3  23874  dyaddisjlem  23884  vitalilem2  23898  itg1ge0  23975  mbfi1fseqlem3  24006  xrge0f  24020  itg2seq  24031  itg2monolem1  24039  itg2addlem  24047  itg2gt0  24049  iblcnlem  24077  itgss3  24103  itgsplit  24124  dvnff  24208  dvferm2  24272  dvlip2  24280  dveq0  24285  dvge0  24291  dvcnvre  24304  dvfsumle  24306  dvfsumabs  24308  dvfsumlem2  24312  ftc1lem2  24321  ftc1lem4  24324  ftc1lem5  24325  ftc1cn  24328  ftc2  24329  itgsubstlem  24333  coe1mul3  24381  ply1divex  24418  dgrlem  24507  dgrlb  24514  coemulhi  24532  dgrlt  24544  dgrmul  24548  plydivlem4  24573  fta1  24585  aaliou2b  24618  taylplem2  24640  dvtaylp  24646  ulmcau  24671  tanabsge  24780  sinq12gt0  24781  argimgt0  24881  cxplea  24965  cxple2  24966  cxpsqrt  24972  cxpaddlelem  25018  loglesqrt  25025  logrec  25027  ang180lem2  25074  lawcos  25080  asinlem3a  25134  asinlem3  25135  asinsin  25156  atanlogaddlem  25177  atanlogadd  25178  atanlogsub  25180  atantan  25187  atanbnd  25190  atantayl2  25202  leibpilem1  25204  efrlim  25234  wilthlem2  25333  basellem2  25346  sqfpc  25401  ppieq0  25440  sqff1o  25446  fsumdvdscom  25449  ppiub  25467  chpeq0  25471  chtleppi  25473  fsumvma  25476  fsumvma2  25477  mersenne  25490  dchrabs2  25525  dchr1re  25526  dchrpt  25530  lgsdilem  25587  lgsdinn0  25608  gausslemma2dlem0b  25620  gausslemma2dlem1a  25628  gausslemma2dlem5  25634  gausslemma2dlem6  25635  lgsquad3  25650  m1lgs  25651  2lgslem1a  25654  2lgslem1  25657  2lgslem3a1  25663  2lgslem3b1  25664  2lgslem3c1  25665  2lgslem3d1  25666  2sqlem6  25686  rpvmasumlem  25750  dchrisumlem3  25754  dchrisum0flblem1  25771  pntibndlem2a  25853  pntlem3  25872  padicabv  25893  ercgrg  25990  tglnunirn  26021  tglineeltr  26104  mirln2  26150  mirbtwnhl  26153  isperp2  26188  outpasch  26228  lnopp2hpgb  26236  dfcgrg2  26337  ttgbtwnid  26358  axcontlem2  26439  axcontlem12  26449  elntg2  26459  upgredg  26610  fusgrfisstep  26799  nbupgrres  26834  usgrnbcnvfv  26835  nbusgredgeu  26836  nbcplgr  26904  cusgrexi  26913  structtocusgr  26916  cusgrsizeinds  26922  vtxdgoddnumeven  27023  uhgr0edg0rgr  27043  wlkl1loop  27107  upgriswlk  27110  usgr2pthlem  27236  cyclnspth  27273  wwlknvtx  27315  wspthnp  27320  elwwlks2ons3  27426  elwspths2on  27431  usgr2wspthons3  27435  clwlkclwwlklem2a4  27467  clwlkclwwlk2  27473  clwlkclwwlkfolem  27477  clwlkclwwlkf1  27480  clwwisshclwws  27485  loopclwwlkn1b  27512  clwwlkf1  27520  wwlksext2clwwlk  27528  clwwnisshclwwsn  27530  eleclclwwlknlem2  27532  1pthon2v  27624  upgr3v3e3cycl  27651  upgreupthi  27679  eupth2lemb  27709  frgrncvvdeqlem7  27781  frgrncvvdeqlem8  27782  frgrncvvdeqlem9  27783  clwwnonrepclwwnon  27821  numclwwlkovh  27849  numclwwlk2lem1  27852  frgrreggt1  27869  frgrregord013  27871  cnnv  28150  nmounbseqi  28250  nmounbseqiALT  28251  nmlnogt0  28270  nmblolbii  28272  blocnilem  28277  ajmoi  28331  minvecolem4  28353  hhnv  28638  norm1  28722  hhssnv  28737  pjhtheu  28867  pjpreeq  28871  spanunsni  29052  fh1  29091  fh2  29092  cm2j  29093  chscllem4  29113  pjid  29168  adjmo  29305  eleigveccl  29432  eigvalcl  29434  eigvec1  29435  eighmre  29436  eighmorth  29437  nmop0h  29464  nmbdoplbi  29497  nmcoplbi  29501  nmophmi  29504  lncnopbd  29510  nmbdfnlbi  29522  nmcfnlbi  29525  cnlnadjeui  29550  branmfn  29578  rnbra  29580  nmopleid  29612  strlem5  29728  hstrlem5  29736  dmdbr3  29778  dmdbr4  29779  mdsl3  29789  hatomistici  29835  cvexchlem  29841  chirredlem1  29863  chirredlem2  29864  chirredi  29867  atcvat3i  29869  atcvat4i  29870  atabsi  29874  mdsymlem1  29876  mdsymlem3  29878  mdsymlem5  29880  dmdbr5ati  29895  cdj1i  29906  opreu2reuALT  29937  foresf1o  29962  rabfodom  29963  elabreximd  29967  elpreq  29984  iunrnmptss  30012  f1o3d  30067  acunirnmpt2f  30101  disjdsct  30131  1stpreimas  30134  fcobij  30151  fpwrelmapffslem  30161  xrofsup  30185  eliccelico  30193  elicoelioo  30194  dvdszzq  30220  prmdvdsbc  30221  numdenneg  30222  fsumiunle  30234  dpadd3  30277  threehalves  30280  s3f1  30308  pfxlsw2ccat  30310  wrdt2ind  30311  cshf1o  30315  xrge0addgt0  30357  xrge0adddir  30358  xrge0npcan  30360  omndmul3  30379  symgcom  30391  pmtrcnel  30397  pmtrcnel2  30398  pmtrcnelor  30399  tocyc01  30412  trsp2cyc  30417  cycpmrn  30427  tocyccntz  30428  cyc3evpm  30435  cyc3genpmlem  30436  cyc3genpm  30437  cycpmgcl  30438  cycpmconjslem2  30440  cycpmconjs  30441  cyc3conja  30442  submarchi  30458  archirng  30460  archirngz  30461  archiexdiv  30462  archiabllem1a  30463  imaslmod  30581  linds2eq  30592  lvecdimfi  30607  lvecdim0i  30613  lssdimle  30615  dimpropd  30616  lbslsat  30623  lindsunlem  30629  lbsdiflsp0  30631  dimkerim  30632  fedgmullem1  30634  fedgmullem2  30635  fedgmul  30636  extdg1id  30662  1smat1  30689  madjusmdetlem2  30713  locfinreflem  30726  metideq  30755  unitdivcld  30766  cnre2csqlem  30775  ordtconnlem1  30789  fmcncfil  30796  lmxrge0  30817  pl1cn  30820  zrhunitpreima  30841  qqhval2lem  30844  qqhf  30849  indf1ofs  30907  esumfsup  30951  esumpcvgval  30959  esum2dlem  30973  esum2d  30974  esumiun  30975  sigasspw  30997  issgon  31004  ispisys2  31034  meascnbl  31100  voliune  31110  volfiniune  31111  omssubaddlem  31179  carsggect  31198  carsgclctunlem2  31199  oddpwdc  31234  eulerpartlems  31240  eulerpartlemgvv  31256  ballotlemfrcn0  31409  sgncl  31418  sgnneg  31420  sgn3da  31421  sgnmul  31422  sgnsub  31424  gsumnunsn  31433  signsplypnf  31442  signsply0  31443  signslema  31454  signstfvneq0  31464  signsvfpn  31477  signsvfnn  31478  repr0  31504  reprlt  31512  reprgt  31514  reprinfz1  31515  chtvalz  31522  breprexplemc  31525  hgt750lemb  31549  hgt750leme  31551  lpadlem3  31571  bnj563  31636  bnj1001  31851  revwlk  31987  spthcycl  31990  usgrgt2cycl  31991  umgracycusgr  32015  subfacp1lem5  32045  subfacp1lem6  32046  erdszelem9  32060  ptpconn  32094  resconn  32107  cvmlift3lem7  32186  satfv1  32224  fmlasuc  32247  satffunlem1lem2  32264  satffunlem2lem2  32267  satefvfmla0  32279  msrrcl  32404  trpredrec  32692  scutbdaylt  32891  btwnintr  33095  btwnouttr  33100  cgrxfr  33131  btwnconn1lem12  33174  colinbtwnle  33194  lineelsb2  33224  nn0prpwlem  33285  neibastop3  33325  onintopssconn  33403  bj-restsnss  33998  bj-restsnss2  33999  taupilem1  34158  relowlssretop  34200  finxpsuclem  34234  unccur  34431  lindsenlbs  34443  matunitlindflem1  34444  matunitlindflem2  34445  poimirlem2  34450  poimirlem8  34456  poimirlem14  34462  poimirlem15  34463  poimirlem17  34465  poimirlem20  34468  poimirlem22  34470  poimirlem24  34472  poimirlem25  34473  poimirlem27  34475  poimirlem28  34476  poimirlem31  34479  heicant  34483  mblfinlem2  34486  itg2gt0cn  34503  itgaddnclem2  34507  ftc1cnnclem  34521  ftc1cnnc  34522  ftc1anclem2  34524  ftc1anclem5  34527  ftc1anclem7  34529  ftc1anc  34531  ftc2nc  34532  dvasin  34534  areacirclem5  34542  areacirc  34543  fdc  34577  incsequz  34580  blbnd  34622  prdstotbnd  34629  cnpwstotbnd  34632  ismtyres  34643  rngohomf  34801  rngohom1  34803  rngohomadd  34804  rngohommul  34805  idlss  34851  idl0cl  34853  idladdcl  34854  idllmulcl  34855  idlrmulcl  34856  maxidlnr  34877  maxidlmax  34878  smprngopr  34887  pridlc  34906  ac6s6f  35008  eqvrelth  35402  lshpnel2N  35677  islsati  35686  lkr0f  35786  lfl1dim  35813  lfl1dim2N  35814  omlfh1N  35950  leat  35985  atlatmstc  36011  cvlatexch3  36030  lnnat  36119  cvrat3  36134  cvrat4  36135  3dim3  36161  dalem4  36357  dalem39  36403  paddasslem12  36523  psubcliN  36630  pmapojoinN  36660  lhpm0atN  36721  lhprelat3N  36732  trlnid  36871  trlval3  36879  cdleme22b  37033  trljco  37432  diaglbN  37747  dibvalrel  37855  dicvalrelN  37877  diclspsn  37886  dih1dimatlem  38021  dihlatat  38029  lcfl6  38192  lcfl8  38194  lcfrvalsnN  38233  lcfrlem9  38242  mapdheq2  38421  hlhillcs  38650  hlhilhillem  38652  fzosumm1  38681  frlmsnic  38701  mzpindd  38853  lzunuz  38875  2rexfrabdioph  38903  irrapxlem3  38931  pellexlem2  38937  pellexlem5  38940  pell1234qrreccl  38961  pell14qrdich  38976  pell1qrge1  38977  elpell1qr2  38979  reglogltb  38998  reglogleb  38999  rmxycomplete  39024  2nn0ind  39052  congabseq  39081  acongrep  39087  acongeq  39090  jm2.22  39102  jm2.26lem3  39108  pw2f1ocnv  39144  limsuc2  39151  fnwe2lem3  39162  aomclem6  39169  kercvrlsm  39193  pwssplit4  39199  lpirlnr  39227  rfovcnvf1od  39860  dssmapnvod  39876  cvgdvgrat  40208  radcnvrat  40209  dvconstbi  40229  bccbc  40240  bi2imp  40380  ax6e2ndeqALT  40829  mulltgt0  40843  refsumcn  40851  cncmpmax  40853  projf1o  41024  unirnmapsn  41042  icoiccdif  41367  climinf  41454  climreeq  41461  climeldmeq  41513  xlimresdm  41707  coskpi2  41714  cosknegpi  41717  icccncfext  41737  dvmptfprodlem  41796  volioore  41843  stoweidlem27  41880  stoweidlem29  41882  stoweidlem31  41884  stoweidlem34  41887  stoweidlem48  41901  stoweidlem59  41912  fourierdlem109  42068  fourierswlem  42083  elaa2  42087  etransclem37  42124  hspmbllem2  42477  smflimmpt  42652  sigarcol  42689  ndmaovg  42925  afv2orxorb  42969  subsubelfzo0  43068  iccelpart  43101  fargshiftf1  43109  fargshiftfo  43110  sbcpr  43191  reuopreuprim  43196  fmtnoprmfac1lem  43234  fmtno4prmfac  43242  2pwp1prmfmtno  43260  sfprmdvdsmersenne  43276  lighneallem3  43280  proththd  43287  evenm1odd  43312  evenp1odd  43313  nnoALTV  43368  fpprel2  43414  stgoldbwt  43449  sbgoldbst  43451  nnsum4primeseven  43473  nnsum4primesevenALTV  43474  bgoldbtbndlem2  43479  upgrwlkupwlk  43523  rnghmf1o  43678  rnghmsubcsetclem1  43750  zrinitorngc  43775  zrtermorngc  43776  rhmsubcsetclem1  43796  rhmsubcrngclem1  43802  funcringcsetcALTV2lem8  43818  funcringcsetclem8ALTV  43841  zrtermoringc  43845  ply1sclrmsm  43943  lincfsuppcl  43974  zofldiv2  44098  elbigolo1  44124  blennn0em1  44158  blennn0e2  44161  dig2nn0ld  44171  nn0sumshdiglem2  44189  rrxlinesc  44229  rrxlinec  44230  eenglngeehlnm  44233  rrxsphere  44242  itschlc0xyqsol  44261  itscnhlinecirc02plem3  44278