Theorem impbid1 226

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid1.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
impbid1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid1.2	. . 3 ⊢ (𝜒 → 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	impbid 213	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 207

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

This theorem is referenced by:  impbid2  227  iba  532  pm5.61  1008  pm5.71  1035  cad0  1625  19.33b  1892  19.40b  1895  19.9t  2216  axc16gb  2274  equs5  2468  2eu1  2654  2eu1v  2655  2eu3  2657  ceqsalgALT  3467  eqvincg  3586  reuxfrd  3689  2reu1  3829  disjeq0  4384  undif4  4395  iftrueb  4467  ssprsseq  4756  sneqbg  4774  preq1b  4777  opthpr  4782  preq12nebg  4794  opthprneg  4796  dfiun2g  4959  elpwuni  5034  disjxiun  5069  eusv2i  5323  reusv2lem3  5329  reusv3  5334  soltmin  6086  ssxpb  6125  xp11  6126  xpcan  6127  xpcan2  6128  ordssun  6414  suc11  6419  unizlim  6434  imadif  6569  2elresin  6606  mpteqb  6955  f1fveq  7206  f1elima  7207  f1imass  7208  fliftf  7259  funeldmb  7303  sorpssuni  7675  sorpssint  7676  iunpw  7714  ssonprc  7730  onint0  7734  oa00  8484  omcan  8494  omopth2  8509  oecan  8515  nnarcl  8542  iserd  8660  mapfset  8787  map0g  8822  fundmen  8968  fopwdom  9013  onfin  9139  0sdom1dom  9146  fineqvlem  9166  f1finf1o  9173  isfiniteg  9200  inficl  9328  tc00  9658  cardnueq0  9879  cardsdomel  9889  wdomfil  9974  wdomnumr  9977  alephsucdom  9992  cardalephex  10003  dfac12lem2  10058  cfeq0  10169  fin23lem24  10235  fin1a2lem9  10321  carden  10464  axrepnd  10508  axacndlem4  10524  gchpwdom  10584  gchina  10613  r1tskina  10696  addcanpi  10813  mulcanpi  10814  elnpi  10902  addcan  11321  addcan2  11322  neg11  11436  negreb  11450  add20  11653  mulcand  11774  cru  12142  nn0lt10b  12582  uz11  12804  eqreznegel  12875  lbzbi  12877  rpnnen1lem6  12923  xrmaxlt  13124  xrltmin  13125  xrmaxle  13126  xrlemin  13127  xneg11  13158  xnn0xadd0  13190  xsubge0  13204  xrub  13255  elioc2  13353  elico2  13354  elicc2  13355  fzopth  13506  2ffzeq  13594  fzoopth  13708  flidz  13760  addmodlteq  13899  expeq0  14045  sq01  14178  fz1eqb  14307  hashen1  14323  hash1snb  14372  hashle2pr  14430  wrdnval  14498  eqwrd  14510  ccatalpha  14547  wrdl1s1  14568  ccats1alpha  14573  ccatopth  14669  ccatopth2  14670  wrdlen2  14897  cj11  15115  sqrt0  15194  abs00  15242  recan  15290  cnsqrt00  15346  rlimdm  15504  rpnnen2lem12  16183  0dvds  16236  dvds1  16279  alzdvds  16280  nn0enne  16337  nn0oddm1d2  16345  nnoddm1d2  16346  gcdeq0  16477  algcvgblem  16537  2mulprm  16653  prmexpb  16680  prmreclem3  16880  4sqlem11  16917  moni  17694  chnfibg  18593  grprcan  18940  grplcan  18967  grpinv11  18974  grpinv11OLD  18975  galcan  19270  sylow2a  19585  subgdisjb  19659  0ringdif  20499  domnlcanb  20692  domnrcanb  20694  drngmuleq0  20735  fidomndrng  20745  lspsncmp  21109  xrsdsreclb  21389  znidomb  21536  lmisfree  21817  coe1tm  22259  tgdom  22961  en1top  22967  cmpfi  23391  txcmpb  23627  hmeocnvb  23757  flimcls  23968  hauspwpwf1  23970  flftg  23979  ghmcnp  24098  metrest  24507  icoopnst  24924  iocopnst  24925  ishl2  25355  vitali  25598  mbfi1fseqlem4  25703  aannenlem1  26312  perfect  27212  2lgsoddprmlem3  27395  2sq2  27414  ltsval2  27638  bday0b  27823  negs11  28059  elnns2  28351  n0cutlt  28369  umgrislfupgrlem  29209  usgrausgrb  29256  upgriswlk  29727  uhgrwkspth  29841  usgr2wlkspth  29845  usgr2trlspth  29847  usgr2pthspth  29848  extwwlkfab  30440  grporcan  30607  grpolcan  30619  ip2eqi  30945  hial2eq  31195  eigorthi  31926  stge1i  32327  stle0i  32328  mdbr3  32386  mdbr4  32387  atsseq  32436  mdsymlem7  32498  reuxfrdf  32578  disjunsn  32683  fpwrelmapffslem  32824  xmulcand  32999  prsdm  34098  prsrn  34099  lfuhgr  35346  lfuhgr2  35347  mthmpps  35810  untangtr  35942  filnetlem4  36609  ordtopconn  36667  ordtopt0  36670  bj-dfbi6  36886  bj-spvew  36976  bj-19.9htbi  37046  bj-axseprep  37427  bj-elid6  37530  icorempo  37713  inunissunidif  37737  fvineqsneu  37773  wl-lem-moexsb  37939  seqpo  38114  qmapeldisjsbi  39228  lshpcmp  39480  lsatcmp  39495  lsatcmp2  39496  ltrneq2  40640  ltrneq  40641  tendospcanN  41515  dochlkr  41877  lcfl7N  41993  hgmap11  42394  ccatcan2d  42735  remulcan2d  42740  itrere  42795  log11d  42823  resubcan2  42865  readdcan2  42890  sn-addcand  42897  sn-addcan2d  42899  remulcand  42916  sn-itrere  42978  sn-retire  42979  cnreeu  42980  fphpd  43261  pellexlem3  43276  qirropth  43353  expdioph  43468  rpnnen3  43477  iotasbc  44863  f1ocof1ob2  47545  2reu3  47573  rlimdmafv  47640  afv2orxorb  47691  rlimdmafv2  47721  funop1  47746  2ffzoeq  47791  prprelprb  47992  poprelb  47999  evenprm2  48205  perfectALTV  48214  nnsum3primesle9  48285  upgrwlkupwlkb  48632  islinindfis  48940  lincresunit3lem3  48965  blen1b  49079  line2ylem  49242  line2y  49246  intubeu  49474  unilbeu  49475  thincn0eu  49921