Theorem impbid1 228

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  impbid2  229  iba  537  pm5.61  1016  pm5.71  1045  cad0  1651  19.33b  1918  19.40b  1921  19.9t  2240  axc16gb  2296  equs5  2489  2eu1  2675  2eu1v  2676  2eu3  2678  ceqsalgALT  3486  eqvincg  3602  reuxfrd  3706  2reu1  3845  disjeq0  4409  undif4  4420  iftrueb  4495  ssprsseq  4786  sneqbg  4803  preq1b  4806  opthpr  4811  preq12nebg  4823  opthprneg  4825  dfiun2g  4988  elpwuni  5065  disjxiun  5100  eusv2i  5359  reusv2lem3  5365  reusv3  5370  soltmin  6130  ssxpb  6167  xp11  6168  xpcan  6169  xpcan2  6170  ordssun  6462  suc11  6467  unizlim  6482  imadif  6618  2elresin  6654  mpteqb  7007  f1fveq  7260  f1elima  7261  f1imass  7262  fliftf  7317  funeldmb  7363  sorpssuni  7734  sorpssint  7735  iunpw  7771  ssonprc  7787  onint0  7791  oa00  8549  omcan  8559  omopth2  8574  oecan  8580  nnarcl  8607  iserd  8726  mapfset  8854  map0g  8894  fundmen  9041  fopwdom  9086  onfin  9212  0sdom1dom  9219  fineqvlem  9239  f1finf1o  9246  isfiniteg  9273  inficl  9398  tc00  9728  cardnueq0  9972  cardsdomel  9982  wdomfil  10067  wdomnumr  10070  alephsucdom  10085  cardalephex  10096  dfac12lem2  10150  cfeq0  10261  fin23lem24  10327  fin1a2lem9  10413  carden  10562  axrepnd  10606  axacndlem4  10622  gchpwdom  10682  gchina  10711  r1tskina  10794  addcanpi  10911  mulcanpi  10912  elnpi  11000  addcan  11421  addcan2  11422  neg11  11536  negreb  11550  add20  11753  mulcand  11874  cru  12237  nn0lt10b  12686  uz11  12915  eqreznegel  12986  lbzbi  12988  rpnnen1lem6  13035  xrmaxlt  13236  xrltmin  13237  xrmaxle  13238  xrlemin  13239  xneg11  13270  xnn0xadd0  13302  xsubge0  13316  xrub  13367  elioc2  13465  elico2  13466  elicc2  13467  fzopth  13619  2ffzeq  13707  fzoopth  13821  flidz  13874  addmodlteq  14013  expeq0  14159  sq01  14292  fz1eqb  14421  hashen1  14437  hash1snb  14487  hashle2pr  14545  wrdnval  14613  eqwrd  14625  ccatalpha  14663  wrdl1s1  14685  ccats1alpha  14690  ccatopth  14788  ccatopth2  14789  wrdlen2  15018  cj11  15252  sqrt0  15331  abs00  15379  recan  15427  cnsqrt00  15483  rlimdm  15641  rpnnen2lem12  16316  0dvds  16369  dvds1  16412  alzdvds  16413  nn0enne  16470  nn0oddm1d2  16478  nnoddm1d2  16479  gcdeq0  16610  algcvgblem  16670  2mulprm  16786  prmexpb  16813  prmreclem3  17013  4sqlem11  17050  moni  17828  chnfibg  18727  grprcan  19100  grplcan  19127  grpinv11  19134  galcan  19434  sylow2a  19749  subgdisjb  19823  0ringdif  20691  domnlcanb  20884  domnrcanb  20886  drngmuleq0  20932  fidomndrng  20943  lspsncmp  21306  xrsdsreclb  21630  znidomb  21777  lmisfree  22058  coe1tm  22502  tgdom  23206  en1top  23212  cmpfi  23636  txcmpb  23873  hmeocnvb  24003  flimcls  24214  hauspwpwf1  24216  flftg  24225  ghmcnp  24344  metrest  24753  icoopnst  25170  iocopnst  25171  ishl2  25601  vitali  25844  mbfi1fseqlem4  25949  aannenlem1  26567  perfect  27470  2lgsoddprmlem3  27653  2sq2  27672  ltsval2  27895  bday0b  28081  negs11  28317  elnns2  28609  n0cutlt  28627  umgrislfupgrlem  29582  lfuhgr  29608  lfuhgr2  29609  usgrausgrb  29632  upgriswlk  30103  uhgrwkspth  30223  usgr2wlkspth  30227  usgr2trlspth  30229  usgr2pthspth  30230  extwwlkfab  30835  grporcan  31002  grpolcan  31014  ip2eqi  31340  hial2eq  31590  eigorthi  32321  stge1i  32722  stle0i  32723  mdbr3  32781  mdbr4  32782  atsseq  32831  mdsymlem7  32893  reuxfrdf  32969  disjunsn  33070  fpwrelmapffslem  33206  xmulcand  33369  prsdm  34427  prsrn  34428  mthmpps  36164  untangtr  36296  filnetlem4  37003  ordtopconn  37061  ordtopt0  37064  bj-dfbi6  37279  bj-spvew  37369  bj-19.9htbi  37439  bj-axseprep  37822  bj-elid6  37925  icorempo  38108  inunissunidif  38132  fvineqsneu  38168  wl-lem-moexsb  38334  seqpo  38500  qmapeldisjsbi  39612  lshpcmp  39864  lsatcmp  39879  lsatcmp2  39880  ltrneq2  41024  ltrneq  41025  tendospcanN  41899  dochlkr  42261  lcfl7N  42377  hgmap11  42778  ccatcan2d  43121  remulcan2d  43126  itrere  43196  log11d  43224  resubcan2  43266  readdcan2  43291  sn-addcand  43298  sn-addcan2d  43300  remulcand  43317  sn-itrere  43379  sn-retire  43380  cnreeu  43381  fphpd  43660  pellexlem3  43675  qirropth  43752  expdioph  43867  rpnnen3  43876  iotasbc  45246  f1ocof1ob2  47973  2reu3  48001  rlimdmafv  48068  afv2orxorb  48119  rlimdmafv2  48149  funop1  48174  2ffzoeq  48219  prprelprb  48420  poprelb  48427  evenprm2  48633  perfectALTV  48642  nnsum3primesle9  48713  upgrwlkupwlkb  49060  islinindfis  49382  lincresunit3lem3  49407  blen1b  49521  line2ylem  49684  line2y  49688  intubeu  49913  unilbeu  49914  thincn0eu  50360