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  4757  sneqbg  4773  preq1b  4776  opthpr  4781  preq12nebg  4792  opthprneg  4794  elpwuni  5026  disjxiun  5062  eusv2i  5294  reusv2lem3  5300  reusv3  5305  soltmin  5995  ssxpb  6030  xp11  6031  xpcan  6032  xpcan2  6033  ordssun  6289  suc11  6293  unizlim  6306  imadif  6437  2elresin  6467  mpteqb  6786  f1fveq  7019  f1elima  7020  f1imass  7021  fliftf  7067  sorpssuni  7457  sorpssint  7458  iunpw  7492  ssonprc  7506  onint0  7510  oa00  8184  omcan  8194  omopth2  8209  oecan  8214  nnarcl  8241  iserd  8314  map0g  8447  fundmen  8582  fopwdom  8624  onfin  8708  fineqvlem  8731  f1finf1o  8744  isfiniteg  8777  inficl  8888  tc00  9189  cardnueq0  9392  cardsdomel  9402  wdomfil  9486  wdomnumr  9489  alephsucdom  9504  cardalephex  9515  dfac12lem2  9569  cfeq0  9677  fin23lem24  9743  fin1a2lem9  9829  carden  9972  axrepnd  10015  axacndlem4  10031  gchpwdom  10091  gchina  10120  r1tskina  10203  addcanpi  10320  mulcanpi  10321  elnpi  10409  addcan  10823  addcan2  10824  neg11  10936  negreb  10950  add20  11151  mulcand  11272  cru  11629  nn0lt10b  12043  uz11  12266  eqreznegel  12333  lbzbi  12335  rpnnen1lem6  12380  xrmaxlt  12573  xrltmin  12574  xrmaxle  12575  xrlemin  12576  xneg11  12607  xnn0xadd0  12639  xsubge0  12653  xrub  12704  elioc2  12798  elico2  12799  elicc2  12800  fzopth  12943  2ffzeq  13027  flidz  13179  addmodlteq  13313  expeq0  13458  sq01  13585  fz1eqb  13714  hashen1  13730  hash1snb  13779  hashle2pr  13834  wrdnval  13895  eqwrd  13908  ccatalpha  13946  wrdl1s1  13967  ccats1alpha  13972  ccatopth  14077  ccatopth2  14078  wrdlen2  14305  cj11  14520  sqrt0  14600  abs00  14648  recan  14695  cnsqrt00  14751  rlimdm  14907  rpnnen2lem12  15577  0dvds  15629  dvds1  15668  alzdvds  15669  nn0enne  15727  nn0oddm1d2  15735  nnoddm1d2  15736  gcdeq0  15864  algcvgblem  15920  2mulprm  16036  prmexpb  16061  prmreclem3  16253  4sqlem11  16290  moni  17005  grprcan  18136  grplcan  18160  grpinv11  18167  galcan  18433  sylow2a  18743  subgdisjb  18818  drngmuleq0  19524  lspsncmp  19887  fidomndrng  20079  coe1tm  20440  xrsdsreclb  20591  znidomb  20707  lmisfree  20985  tgdom  21585  en1top  21591  cmpfi  22015  txcmpb  22251  hmeocnvb  22381  flimcls  22592  hauspwpwf1  22594  flftg  22603  ghmcnp  22722  metrest  23133  icoopnst  23542  iocopnst  23543  ishl2  23972  vitali  24213  mbfi1fseqlem4  24318  aannenlem1  24916  perfect  25806  2lgsoddprmlem3  25989  2sq2  26008  umgrislfupgrlem  26906  usgrausgrb  26953  upgriswlk  27421  uhgrwkspth  27535  usgr2wlkspth  27539  usgr2trlspth  27541  usgr2pthspth  27542  extwwlkfab  28130  grporcan  28294  grpolcan  28306  ip2eqi  28632  hial2eq  28882  eigorthi  29613  stge1i  30014  stle0i  30015  mdbr3  30073  mdbr4  30074  atsseq  30123  mdsymlem7  30185  reuxfrdf  30254  disjunsn  30343  fpwrelmapffslem  30467  xmulcand  30597  prsdm  31157  prsrn  31158  lfuhgr  32364  lfuhgr2  32365  mthmpps  32829  untangtr  32940  funeldmb  33006  sltval2  33163  filnetlem4  33729  ordtopconn  33787  ordtopt0  33790  bj-dfbi6  33908  bj-19.9htbi  34037  bj-elid6  34461  icorempo  34631  inunissunidif  34655  fvineqsneu  34691  wl-lem-moexsb  34803  seqpo  35021  lshpcmp  36123  lsatcmp  36138  lsatcmp2  36139  ltrneq2  37283  ltrneq  37284  tendospcanN  38158  dochlkr  38520  lcfl7N  38636  hgmap11  39037  ccatcan2d  39125  remulcan2d  39154  resubcan2  39216  readdcan2  39240  remulcand  39248  fphpd  39411  pellexlem3  39426  qirropth  39503  expdioph  39618  rpnnen3  39627  iotasbc  40749  2reu3  43308  rlimdmafv  43375  afv2orxorb  43426  rlimdmafv2  43456  funop1  43481  fzoopth  43526  2ffzoeq  43527  prprelprb  43678  poprelb  43685  evenprm2  43878  perfectALTV  43887  nnsum3primesle9  43958  upgrwlkupwlkb  44015  0ringdif  44140  islinindfis  44503  lincresunit3lem3  44528  blen1b  44647  line2ylem  44737  line2y  44741