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  1002  pm5.71  1029  cad0  1619  19.33b  1886  19.40b  1889  19.9t  2207  axc16gb  2265  equs5  2460  2eu1  2646  2eu1v  2647  2eu3  2649  ceqsalgALT  3473  eqvincg  3598  reuxfrd  3702  2reu1  3843  disjeq0  4403  undif4  4414  iftrueb  4485  ssprsseq  4774  sneqbg  4792  preq1b  4795  opthpr  4800  preq12nebg  4812  opthprneg  4814  dfiun2g  4978  elpwuni  5051  disjxiun  5086  eusv2i  5330  reusv2lem3  5336  reusv3  5341  soltmin  6082  ssxpb  6121  xp11  6122  xpcan  6123  xpcan2  6124  ordssun  6410  suc11  6415  unizlim  6430  imadif  6565  2elresin  6602  mpteqb  6948  f1fveq  7196  f1elima  7197  f1imass  7198  fliftf  7249  funeldmb  7293  sorpssuni  7665  sorpssint  7666  iunpw  7704  ssonprc  7720  onint0  7724  oa00  8474  omcan  8484  omopth2  8499  oecan  8504  nnarcl  8531  iserd  8648  mapfset  8774  map0g  8808  fundmen  8953  fopwdom  8998  onfin  9124  0sdom1dom  9130  fineqvlem  9150  f1finf1o  9157  isfiniteg  9184  inficl  9309  tc00  9636  cardnueq0  9857  cardsdomel  9867  wdomfil  9952  wdomnumr  9955  alephsucdom  9970  cardalephex  9981  dfac12lem2  10036  cfeq0  10147  fin23lem24  10213  fin1a2lem9  10299  carden  10442  axrepnd  10485  axacndlem4  10501  gchpwdom  10561  gchina  10590  r1tskina  10673  addcanpi  10790  mulcanpi  10791  elnpi  10879  addcan  11297  addcan2  11298  neg11  11412  negreb  11426  add20  11629  mulcand  11750  cru  12117  nn0lt10b  12535  uz11  12757  eqreznegel  12832  lbzbi  12834  rpnnen1lem6  12880  xrmaxlt  13080  xrltmin  13081  xrmaxle  13082  xrlemin  13083  xneg11  13114  xnn0xadd0  13146  xsubge0  13160  xrub  13211  elioc2  13309  elico2  13310  elicc2  13311  fzopth  13461  2ffzeq  13549  fzoopth  13662  flidz  13714  addmodlteq  13853  expeq0  13999  sq01  14132  fz1eqb  14261  hashen1  14277  hash1snb  14326  hashle2pr  14384  wrdnval  14452  eqwrd  14464  ccatalpha  14501  wrdl1s1  14522  ccats1alpha  14527  ccatopth  14623  ccatopth2  14624  wrdlen2  14851  cj11  15069  sqrt0  15148  abs00  15196  recan  15244  cnsqrt00  15300  rlimdm  15458  rpnnen2lem12  16134  0dvds  16187  dvds1  16230  alzdvds  16231  nn0enne  16288  nn0oddm1d2  16296  nnoddm1d2  16297  gcdeq0  16428  algcvgblem  16488  2mulprm  16604  prmexpb  16630  prmreclem3  16830  4sqlem11  16867  moni  17643  chnfibg  18542  grprcan  18886  grplcan  18913  grpinv11  18920  grpinv11OLD  18921  galcan  19216  sylow2a  19531  subgdisjb  19605  0ringdif  20442  domnlcanb  20635  domnrcanb  20637  drngmuleq0  20678  fidomndrng  20688  lspsncmp  21053  xrsdsreclb  21350  znidomb  21498  lmisfree  21779  coe1tm  22187  tgdom  22893  en1top  22899  cmpfi  23323  txcmpb  23559  hmeocnvb  23689  flimcls  23900  hauspwpwf1  23902  flftg  23911  ghmcnp  24030  metrest  24439  icoopnst  24863  iocopnst  24864  ishl2  25297  vitali  25541  mbfi1fseqlem4  25646  aannenlem1  26263  perfect  27169  2lgsoddprmlem3  27352  2sq2  27371  sltval2  27595  bday0b  27774  negs11  27991  elnns2  28269  n0cutlt  28285  umgrislfupgrlem  29100  usgrausgrb  29147  upgriswlk  29619  uhgrwkspth  29733  usgr2wlkspth  29737  usgr2trlspth  29739  usgr2pthspth  29740  extwwlkfab  30332  grporcan  30498  grpolcan  30510  ip2eqi  30836  hial2eq  31086  eigorthi  31817  stge1i  32218  stle0i  32219  mdbr3  32277  mdbr4  32278  atsseq  32327  mdsymlem7  32389  reuxfrdf  32470  disjunsn  32574  fpwrelmapffslem  32715  xmulcand  32901  prsdm  33927  prsrn  33928  lfuhgr  35162  lfuhgr2  35163  mthmpps  35626  untangtr  35758  filnetlem4  36425  ordtopconn  36483  ordtopt0  36486  bj-dfbi6  36619  bj-19.9htbi  36747  bj-elid6  37214  icorempo  37395  inunissunidif  37419  fvineqsneu  37455  wl-lem-moexsb  37612  seqpo  37797  lshpcmp  39097  lsatcmp  39112  lsatcmp2  39113  ltrneq2  40257  ltrneq  40258  tendospcanN  41132  dochlkr  41494  lcfl7N  41610  hgmap11  42011  ccatcan2d  42354  remulcan2d  42360  itrere  42421  log11d  42449  resubcan2  42491  readdcan2  42516  sn-addcand  42523  sn-addcan2d  42525  remulcand  42542  sn-itrere  42591  sn-retire  42592  cnreeu  42593  fphpd  42919  pellexlem3  42934  qirropth  43011  expdioph  43126  rpnnen3  43135  iotasbc  44522  f1ocof1ob2  47192  2reu3  47220  rlimdmafv  47287  afv2orxorb  47338  rlimdmafv2  47368  funop1  47393  2ffzoeq  47437  prprelprb  47627  poprelb  47634  evenprm2  47824  perfectALTV  47833  nnsum3primesle9  47904  upgrwlkupwlkb  48251  islinindfis  48560  lincresunit3lem3  48585  blen1b  48699  line2ylem  48862  line2y  48866  intubeu  49094  unilbeu  49095  thincn0eu  49542