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  2241  axc16gb  2297  equs5  2490  2eu1  2676  2eu1v  2677  2eu3  2679  ceqsalgALT  3487  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  5356  reusv2lem3  5362  reusv3  5367  elrelb  5775  soltmin  6130  ssxpb  6166  xp11  6167  xpcan  6168  xpcan2  6169  ordssun  6467  suc11  6472  unizlim  6487  imadif  6624  2elresin  6660  mpteqb  7013  f1fveq  7266  f1elima  7267  f1imass  7268  fliftf  7323  funeldmb  7369  sorpssuni  7748  sorpssint  7749  iunpw  7785  ssonprc  7801  onint0  7805  oa00  8567  omcan  8577  omopth2  8592  oecan  8598  nnarcl  8625  iserd  8744  mapfset  8872  map0g  8912  fundmen  9059  fopwdom  9104  onfin  9230  0sdom1dom  9237  fineqvlem  9257  f1finf1o  9264  isfiniteg  9292  inficl  9417  tc00  9747  cardnueq0  10045  cardsdomel  10055  wdomfil  10140  wdomnumr  10143  alephsucdom  10158  cardalephex  10169  dfac12lem2  10223  cfeq0  10334  fin23lem24  10400  fin1a2lem9  10486  carden  10635  axrepnd  10679  axacndlem4  10695  gchpwdom  10755  gchina  10784  r1tskina  10867  addcanpi  10984  mulcanpi  10985  elnpi  11073  addcan  11494  addcan2  11495  neg11  11609  negreb  11623  add20  11828  mulcand  11949  cru  12312  nn0lt10b  12761  uz11  12990  eqreznegel  13061  lbzbi  13063  rpnnen1lem6  13110  xrmaxlt  13311  xrltmin  13312  xrmaxle  13313  xrlemin  13314  xneg11  13345  xnn0xadd0  13377  xsubge0  13391  xrub  13442  elioc2  13540  elico2  13541  elicc2  13542  fzopth  13695  2ffzeq  13783  fzoopth  13897  flidz  13950  addmodlteq  14089  expeq0  14235  sq01  14369  fz1eqb  14498  hashen1  14514  hash1snb  14564  hashle2pr  14622  wrdnval  14690  eqwrd  14702  ccatalpha  14740  wrdl1s1  14762  ccats1alpha  14767  ccatopth  14865  ccatopth2  14866  wrdlen2  15095  cj11  15329  sqrt0  15408  abs00  15456  recan  15504  cnsqrt00  15560  rlimdm  15718  rpnnen2lem12  16393  0dvds  16446  dvds1  16489  alzdvds  16490  nn0enne  16547  nn0oddm1d2  16555  nnoddm1d2  16556  gcdeq0  16689  algcvgblem  16752  2mulprm  16868  prmexpb  16895  prmreclem3  17096  4sqlem11  17133  moni  17911  chnfibg  18810  grprcan  19184  grplcan  19211  grpinv11  19218  galcan  19518  sylow2a  19833  subgdisjb  19907  0ringdif  20778  domnlcanb  20971  domnrcanb  20973  drngmuleq0  21020  fidomndrng  21031  lspsncmp  21394  xrsdsreclb  21720  znidomb  21867  lmisfree  22148  coe1tm  22592  tgdom  23296  en1top  23302  cmpfi  23726  txcmpb  23963  hmeocnvb  24093  flimcls  24304  hauspwpwf1  24306  flftg  24315  ghmcnp  24434  metrest  24843  icoopnst  25260  iocopnst  25261  ishl2  25691  vitali  25934  mbfi1fseqlem4  26039  aannenlem1  26655  perfect  27558  2lgsoddprmlem3  27741  2sq2  27760  ltsval2  28013  bday0b  28199  negs11  28435  elnns2  28727  n0cutlt  28745  umgrislfupgrlem  29700  lfuhgr  29726  lfuhgr2  29727  usgrausgrb  29750  upgriswlk  30221  uhgrwkspth  30341  usgr2wlkspth  30345  usgr2trlspth  30347  usgr2pthspth  30348  extwwlkfab  30953  grporcan  31120  grpolcan  31132  ip2eqi  31458  hial2eq  31708  eigorthi  32439  stge1i  32840  stle0i  32841  mdbr3  32899  mdbr4  32900  atsseq  32949  mdsymlem7  33011  reuxfrdf  33087  disjunsn  33188  fpwrelmapffslem  33324  xmulcand  33487  prsdm  34546  prsrn  34547  infinfnum  35757  mthmpps  36347  untangtr  36479  filnetlem4  37169  ordtopconn  37227  ordtopt0  37230  bj-dfbi6  37445  bj-spvew  37535  bj-19.9htbi  37605  bj-axseprep  37990  bj-elid6  38091  icorempo  38274  inunissunidif  38298  fvineqsneu  38334  wl-lem-moexsb  38500  seqpo  38681  qmapeldisjsbi  39793  lshpcmp  40045  lsatcmp  40060  lsatcmp2  40061  ltrneq2  41205  ltrneq  41206  tendospcanN  42080  dochlkr  42442  lcfl7N  42558  hgmap11  42959  ccatcan2d  43302  remulcan2d  43307  itrere  43375  log11d  43397  resubcan2  43439  readdcan2  43464  sn-addcand  43471  sn-addcan2d  43473  remulcand  43490  sn-itrere  43552  sn-retire  43553  cnreeu  43554  fphpd  43822  pellexlem3  43837  qirropth  43914  expdioph  44029  rpnnen3  44038  iotasbc  45402  cocanss2  45921  f1ocof1ob2  48151  2reu3  48179  rlimdmafv  48246  afv2orxorb  48297  rlimdmafv2  48327  funop1  48352  2ffzoeq  48397  prprelprb  48598  poprelb  48605  evenprm2  48811  perfectALTV  48820  nnsum3primesle9  48891  upgrwlkupwlkb  49238  islinindfis  49560  lincresunit3lem3  49585  blen1b  49699  line2ylem  49862  line2y  49866  intubeu  50091  unilbeu  50092  thincn0eu  50538