Theorem impbid1 225

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 212	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  impbid2  226  iba  527  pm5.61  1003  pm5.71  1030  cad0  1620  19.33b  1887  19.40b  1890  19.9t  2212  axc16gb  2270  equs5  2465  2eu1  2652  2eu1v  2653  2eu3  2655  ceqsalgALT  3479  eqvincg  3604  reuxfrd  3708  2reu1  3849  disjeq0  4410  undif4  4421  iftrueb  4494  ssprsseq  4783  sneqbg  4801  preq1b  4804  opthpr  4809  preq12nebg  4821  opthprneg  4823  dfiun2g  4987  elpwuni  5062  disjxiun  5097  eusv2i  5341  reusv2lem3  5347  reusv3  5352  soltmin  6101  ssxpb  6140  xp11  6141  xpcan  6142  xpcan2  6143  ordssun  6429  suc11  6434  unizlim  6449  imadif  6584  2elresin  6621  mpteqb  6969  f1fveq  7218  f1elima  7219  f1imass  7220  fliftf  7271  funeldmb  7315  sorpssuni  7687  sorpssint  7688  iunpw  7726  ssonprc  7742  onint0  7746  oa00  8496  omcan  8506  omopth2  8521  oecan  8527  nnarcl  8554  iserd  8672  mapfset  8799  map0g  8834  fundmen  8980  fopwdom  9025  onfin  9151  0sdom1dom  9158  fineqvlem  9178  f1finf1o  9185  isfiniteg  9212  inficl  9340  tc00  9667  cardnueq0  9888  cardsdomel  9898  wdomfil  9983  wdomnumr  9986  alephsucdom  10001  cardalephex  10012  dfac12lem2  10067  cfeq0  10178  fin23lem24  10244  fin1a2lem9  10330  carden  10473  axrepnd  10517  axacndlem4  10533  gchpwdom  10593  gchina  10622  r1tskina  10705  addcanpi  10822  mulcanpi  10823  elnpi  10911  addcan  11329  addcan2  11330  neg11  11444  negreb  11458  add20  11661  mulcand  11782  cru  12149  nn0lt10b  12566  uz11  12788  eqreznegel  12859  lbzbi  12861  rpnnen1lem6  12907  xrmaxlt  13108  xrltmin  13109  xrmaxle  13110  xrlemin  13111  xneg11  13142  xnn0xadd0  13174  xsubge0  13188  xrub  13239  elioc2  13337  elico2  13338  elicc2  13339  fzopth  13489  2ffzeq  13577  fzoopth  13690  flidz  13742  addmodlteq  13881  expeq0  14027  sq01  14160  fz1eqb  14289  hashen1  14305  hash1snb  14354  hashle2pr  14412  wrdnval  14480  eqwrd  14492  ccatalpha  14529  wrdl1s1  14550  ccats1alpha  14555  ccatopth  14651  ccatopth2  14652  wrdlen2  14879  cj11  15097  sqrt0  15176  abs00  15224  recan  15272  cnsqrt00  15328  rlimdm  15486  rpnnen2lem12  16162  0dvds  16215  dvds1  16258  alzdvds  16259  nn0enne  16316  nn0oddm1d2  16324  nnoddm1d2  16325  gcdeq0  16456  algcvgblem  16516  2mulprm  16632  prmexpb  16658  prmreclem3  16858  4sqlem11  16895  moni  17672  chnfibg  18571  grprcan  18918  grplcan  18945  grpinv11  18952  grpinv11OLD  18953  galcan  19248  sylow2a  19563  subgdisjb  19637  0ringdif  20475  domnlcanb  20668  domnrcanb  20670  drngmuleq0  20711  fidomndrng  20721  lspsncmp  21086  xrsdsreclb  21383  znidomb  21531  lmisfree  21812  coe1tm  22230  tgdom  22937  en1top  22943  cmpfi  23367  txcmpb  23603  hmeocnvb  23733  flimcls  23944  hauspwpwf1  23946  flftg  23955  ghmcnp  24074  metrest  24483  icoopnst  24907  iocopnst  24908  ishl2  25341  vitali  25585  mbfi1fseqlem4  25690  aannenlem1  26307  perfect  27213  2lgsoddprmlem3  27396  2sq2  27415  ltsval2  27639  bday0b  27824  negs11  28060  elnns2  28352  n0cutlt  28370  umgrislfupgrlem  29211  usgrausgrb  29258  upgriswlk  29730  uhgrwkspth  29844  usgr2wlkspth  29848  usgr2trlspth  29850  usgr2pthspth  29851  extwwlkfab  30443  grporcan  30610  grpolcan  30622  ip2eqi  30948  hial2eq  31198  eigorthi  31929  stge1i  32330  stle0i  32331  mdbr3  32389  mdbr4  32390  atsseq  32439  mdsymlem7  32501  reuxfrdf  32581  disjunsn  32685  fpwrelmapffslem  32826  xmulcand  33017  prsdm  34096  prsrn  34097  lfuhgr  35338  lfuhgr2  35339  mthmpps  35802  untangtr  35934  filnetlem4  36601  ordtopconn  36659  ordtopt0  36662  bj-dfbi6  36804  bj-spvew  36883  bj-19.9htbi  36952  bj-axseprep  37326  bj-elid6  37429  icorempo  37610  inunissunidif  37634  fvineqsneu  37670  wl-lem-moexsb  37827  seqpo  38002  qmapeldisjsbi  39116  lshpcmp  39368  lsatcmp  39383  lsatcmp2  39384  ltrneq2  40528  ltrneq  40529  tendospcanN  41403  dochlkr  41765  lcfl7N  41881  hgmap11  42282  ccatcan2d  42625  remulcan2d  42631  itrere  42692  log11d  42720  resubcan2  42762  readdcan2  42787  sn-addcand  42794  sn-addcan2d  42796  remulcand  42813  sn-itrere  42862  sn-retire  42863  cnreeu  42864  fphpd  43177  pellexlem3  43192  qirropth  43269  expdioph  43384  rpnnen3  43393  iotasbc  44779  f1ocof1ob2  47446  2reu3  47474  rlimdmafv  47541  afv2orxorb  47592  rlimdmafv2  47622  funop1  47647  2ffzoeq  47691  prprelprb  47881  poprelb  47888  evenprm2  48078  perfectALTV  48087  nnsum3primesle9  48158  upgrwlkupwlkb  48505  islinindfis  48813  lincresunit3lem3  48838  blen1b  48952  line2ylem  49115  line2y  49119  intubeu  49347  unilbeu  49348  thincn0eu  49794