Theorem impbid1 227

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  impbid2  228  iba  530  pm5.61  997  pm5.71  1024  cad0  1614  19.33b  1882  19.40b  1885  19.9t  2200  axc16gb  2259  equs5  2479  2eu1  2731  2eu1OLD  2732  2eu1v  2733  2eu3  2735  2eu3OLD  2736  ceqsalgALT  3530  eqvincg  3640  reuxfrd  3738  2reu1  3880  disjeq0  4404  undif4  4415  ssprsseq  4751  sneqbg  4767  preq1b  4770  opthpr  4775  preq12nebg  4786  opthprneg  4788  elpwuni  5019  disjxiun  5055  eusv2i  5286  reusv2lem3  5292  reusv3  5297  soltmin  5990  ssxpb  6025  xp11  6026  xpcan  6027  xpcan2  6028  ordssun  6284  suc11  6288  unizlim  6301  imadif  6432  2elresin  6462  mpteqb  6781  f1fveq  7014  f1elima  7015  f1imass  7016  fliftf  7062  sorpssuni  7452  sorpssint  7453  iunpw  7487  ssonprc  7501  onint0  7505  oa00  8179  omcan  8189  omopth2  8204  oecan  8209  nnarcl  8236  iserd  8309  map0g  8442  fundmen  8577  fopwdom  8619  onfin  8703  fineqvlem  8726  f1finf1o  8739  isfiniteg  8772  inficl  8883  tc00  9184  cardnueq0  9387  cardsdomel  9397  wdomfil  9481  wdomnumr  9484  alephsucdom  9499  cardalephex  9510  dfac12lem2  9564  cfeq0  9672  fin23lem24  9738  fin1a2lem9  9824  carden  9967  axrepnd  10010  axacndlem4  10026  gchpwdom  10086  gchina  10115  r1tskina  10198  addcanpi  10315  mulcanpi  10316  elnpi  10404  addcan  10818  addcan2  10819  neg11  10931  negreb  10945  add20  11146  mulcand  11267  cru  11624  nn0lt10b  12038  uz11  12261  eqreznegel  12328  lbzbi  12330  rpnnen1lem6  12375  xrmaxlt  12568  xrltmin  12569  xrmaxle  12570  xrlemin  12571  xneg11  12602  xnn0xadd0  12634  xsubge0  12648  xrub  12699  elioc2  12793  elico2  12794  elicc2  12795  fzopth  12938  2ffzeq  13022  flidz  13174  addmodlteq  13308  expeq0  13453  sq01  13580  fz1eqb  13709  hashen1  13725  hash1snb  13774  hashle2pr  13829  wrdnval  13890  eqwrd  13903  ccatalpha  13941  wrdl1s1  13962  ccats1alpha  13967  ccatopth  14072  ccatopth2  14073  wrdlen2  14300  cj11  14515  sqrt0  14595  abs00  14643  recan  14690  cnsqrt00  14746  rlimdm  14902  rpnnen2lem12  15572  0dvds  15624  dvds1  15663  alzdvds  15664  nn0enne  15722  nn0oddm1d2  15730  nnoddm1d2  15731  gcdeq0  15859  algcvgblem  15915  2mulprm  16031  prmexpb  16056  prmreclem3  16248  4sqlem11  16285  moni  17000  grprcan  18131  grplcan  18155  grpinv11  18162  galcan  18428  sylow2a  18738  subgdisjb  18813  drngmuleq0  19519  lspsncmp  19882  fidomndrng  20074  coe1tm  20435  xrsdsreclb  20586  znidomb  20702  lmisfree  20980  tgdom  21580  en1top  21586  cmpfi  22010  txcmpb  22246  hmeocnvb  22376  flimcls  22587  hauspwpwf1  22589  flftg  22598  ghmcnp  22717  metrest  23128  icoopnst  23537  iocopnst  23538  ishl2  23967  vitali  24208  mbfi1fseqlem4  24313  aannenlem1  24911  perfect  25801  2lgsoddprmlem3  25984  2sq2  26003  umgrislfupgrlem  26901  usgrausgrb  26948  upgriswlk  27416  uhgrwkspth  27530  usgr2wlkspth  27534  usgr2trlspth  27536  usgr2pthspth  27537  extwwlkfab  28125  grporcan  28289  grpolcan  28301  ip2eqi  28627  hial2eq  28877  eigorthi  29608  stge1i  30009  stle0i  30010  mdbr3  30068  mdbr4  30069  atsseq  30118  mdsymlem7  30180  reuxfrdf  30249  disjunsn  30338  fpwrelmapffslem  30462  xmulcand  30592  prsdm  31152  prsrn  31153  lfuhgr  32359  lfuhgr2  32360  mthmpps  32824  untangtr  32935  funeldmb  33001  sltval2  33158  filnetlem4  33724  ordtopconn  33782  ordtopt0  33785  bj-dfbi6  33903  bj-19.9htbi  34032  bj-elid6  34456  icorempo  34626  inunissunidif  34650  fvineqsneu  34686  wl-lem-moexsb  34798  seqpo  35016  lshpcmp  36118  lsatcmp  36133  lsatcmp2  36134  ltrneq2  37278  ltrneq  37279  tendospcanN  38153  dochlkr  38515  lcfl7N  38631  hgmap11  39032  ccatcan2d  39120  remulcan2d  39149  resubcan2  39211  readdcan2  39235  remulcand  39243  fphpd  39406  pellexlem3  39421  qirropth  39498  expdioph  39613  rpnnen3  39622  iotasbc  40744  2reu3  43303  rlimdmafv  43370  afv2orxorb  43421  rlimdmafv2  43451  funop1  43476  fzoopth  43521  2ffzoeq  43522  prprelprb  43673  poprelb  43680  evenprm2  43873  perfectALTV  43882  nnsum3primesle9  43953  upgrwlkupwlkb  44010  0ringdif  44135  islinindfis  44498  lincresunit3lem3  44523  blen1b  44642  line2ylem  44732  line2y  44736