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  1920  19.40b  1923  19.9t  2244  axc16gb  2300  equs5  2492  2eu1  2678  2eu1v  2679  2eu3  2681  ceqsalgALT  3490  eqvincg  3605  reuxfrd  3709  2reu1  3849  disjeq0  4412  undif4  4423  iftrueb  4498  ssprsseq  4786  sneqbg  4803  preq1b  4806  opthpr  4811  preq12nebg  4823  opthprneg  4825  dfiun2g  4993  elpwuni  5070  disjxiun  5105  eusv2i  5363  reusv2lem3  5369  reusv3  5374  elrelb  5784  soltmin  6148  ssxpb  6184  xp11  6185  xpcan  6186  xpcan2  6187  ordssun  6493  suc11  6498  unizlim  6513  imadif  6654  2elresin  6690  mpteqb  7044  f1fveq  7297  f1elima  7298  f1imass  7299  fliftf  7354  funeldmb  7400  sorpssuni  7780  sorpssint  7781  iunpw  7817  ssonprc  7835  onint0  7839  oa00  8605  omcan  8615  omopth2  8630  oecan  8636  nnarcl  8663  iserd  8782  mapfset  8910  map0g  8950  fundmen  9097  fopwdom  9142  onfin  9268  0sdom1dom  9275  fineqvlem  9295  f1finf1o  9302  isfiniteg  9330  inficl  9454  tc00  9784  cardnueq0  10082  cardsdomel  10092  wdomfil  10179  wdomnumr  10182  alephsucdom  10197  cardalephex  10208  dfac12lem2  10262  cfeq0  10373  fin23lem24  10439  fin1a2lem9  10525  carden  10674  axrepnd  10718  axacndlem4  10734  gchpwdom  10794  gchina  10823  r1tskina  10906  addcanpi  11023  mulcanpi  11024  elnpi  11112  addcan  11533  addcan2  11534  neg11  11648  negreb  11662  add20  11868  mulcand  11989  cru  12352  nn0lt10b  12801  uz11  13030  eqreznegel  13101  lbzbi  13103  rpnnen1lem6  13150  xrmaxlt  13351  xrltmin  13352  xrmaxle  13353  xrlemin  13354  xneg11  13385  xnn0xadd0  13417  xsubge0  13431  xrub  13482  elioc2  13580  elico2  13581  elicc2  13582  fzopth  13735  2ffzeq  13823  fzoopth  13937  flidz  13990  addmodlteq  14129  expeq0  14275  sq01  14410  fz1eqb  14539  hashen1  14555  hash1snb  14605  hashle2pr  14663  wrdnval  14731  eqwrd  14743  ccatalpha  14781  wrdl1s1  14804  ccats1alpha  14809  ccatopth  14907  ccatopth2  14908  wrdlen2  15138  cj11  15372  sqrt0  15451  abs00  15499  recan  15547  cnsqrt00  15604  rlimdm  15762  rpnnen2lem12  16437  0dvds  16490  dvds1  16533  alzdvds  16534  nn0enne  16591  nn0oddm1d2  16599  nnoddm1d2  16600  gcdeq0  16733  algcvgblem  16796  2mulprm  16912  prmexpb  16939  prmreclem3  17140  4sqlem11  17177  moni  17961  chnfibg  18860  grprcan  19234  grplcan  19261  grpinv11  19268  galcan  19569  sylow2a  19884  subgdisjb  19958  0ringdif  20829  domnlcanb  21022  domnrcanb  21024  drngmuleq0  21071  fidomndrng  21082  lspsncmp  21445  xrsdsreclb  21772  znidomb  21922  lmisfree  22203  coe1tm  22647  tgdom  23351  en1top  23357  cmpfi  23781  txcmpb  24018  hmeocnvb  24148  flimcls  24359  hauspwpwf1  24361  flftg  24370  ghmcnp  24489  metrest  24898  icoopnst  25315  iocopnst  25316  ishl2  25746  vitali  25989  mbfi1fseqlem4  26094  aannenlem1  26712  perfect  27615  2lgsoddprmlem3  27798  2sq2  27817  ltsval2  28070  bday0b  28256  negs11  28492  elnns2  28784  n0cutlt  28802  umgrislfupgrlem  29757  lfuhgr  29783  lfuhgr2  29784  usgrausgrb  29807  upgriswlk  30278  uhgrwkspth  30398  usgr2wlkspth  30402  usgr2trlspth  30404  usgr2pthspth  30405  extwwlkfab  31010  grporcan  31177  grpolcan  31189  ip2eqi  31515  hial2eq  31765  eigorthi  32496  stge1i  32897  stle0i  32898  mdbr3  32956  mdbr4  32957  atsseq  33006  mdsymlem7  33068  reuxfrdf  33186  disjunsn  33286  fpwrelmapffslem  33420  xmulcand  33583  prsdm  34657  prsrn  34658  infinfnum  35890  maxssj0  36047  mthmpps  36555  untangtr  36694  filnetlem4  37384  ordtopconn  37442  ordtopt0  37445  bj-dfbi6  37660  bj-spvew  37750  bj-19.9htbi  37820  resssres  38178  relssresv  38189  coss1b  38216  coss2b  38218  bj-axseprep  38260  bj-elid6  38359  icorempo  38542  inunissunidif  38566  fvineqsneu  38602  wl-lem-moexsb  38768  seqpo  38947  qmapeldisjsbi  40059  lshpcmp  40311  lsatcmp  40326  lsatcmp2  40327  ltrneq2  41471  ltrneq  41472  tendospcanN  42346  dochlkr  42708  lcfl7N  42824  hgmap11  43225  ccatcan2d  43568  remulcan2d  43573  itrere  43641  log11d  43663  resubcan2  43705  readdcan2  43730  sn-addcand  43737  sn-addcan2d  43739  remulcand  43756  sn-itrere  43818  sn-retire  43819  cnreeu  43820  fphpd  44089  pellexlem3  44104  qirropth  44181  expdioph  44296  rpnnen3  44305  iotasbc  45663  cocanss2  46183  f1ocof1ob2  48425  2reu3  48454  rlimdmafv  48520  afv2orxorb  48571  rlimdmafv2  48601  funop1  48626  2ffzoeq  48671  prprelprb  48872  poprelb  48879  evenprm2  49085  perfectALTV  49094  nnsum3primesle9  49165  upgrwlkupwlkb  49512  islinindfis  49892  lincresunit3lem3  49917  blen1b  50031  line2ylem  50194  line2xlem  50196  line2y  50198  intubeu  50429  unilbeu  50430  thincn0eu  50897