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  1650  19.33b  1919  19.40b  1922  19.9t  2243  axc16gb  2299  equs5  2492  2eu1  2678  2eu1v  2679  2eu3  2681  ceqsalgALT  3489  eqvincg  3604  reuxfrd  3708  2reu1  3848  disjeq0  4411  undif4  4422  iftrueb  4497  ssprsseq  4783  sneqbg  4800  preq1b  4803  opthpr  4808  preq12nebg  4820  opthprneg  4822  dfiun2g  4990  elpwuni  5067  disjxiun  5102  eusv2i  5359  reusv2lem3  5365  reusv3  5370  elrelb  5779  soltmin  6135  ssxpb  6171  xp11  6172  xpcan  6173  xpcan2  6174  ordssun  6473  suc11  6478  unizlim  6493  imadif  6632  2elresin  6668  mpteqb  7021  f1fveq  7273  f1elima  7274  f1imass  7275  fliftf  7330  funeldmb  7376  sorpssuni  7755  sorpssint  7756  iunpw  7792  ssonprc  7808  onint0  7812  oa00  8578  omcan  8588  omopth2  8603  oecan  8609  nnarcl  8636  iserd  8755  mapfset  8883  map0g  8923  fundmen  9070  fopwdom  9115  onfin  9241  0sdom1dom  9248  fineqvlem  9268  f1finf1o  9275  isfiniteg  9303  inficl  9427  tc00  9757  cardnueq0  10055  cardsdomel  10065  wdomfil  10150  wdomnumr  10153  alephsucdom  10168  cardalephex  10179  dfac12lem2  10233  cfeq0  10344  fin23lem24  10410  fin1a2lem9  10496  carden  10645  axrepnd  10689  axacndlem4  10705  gchpwdom  10765  gchina  10794  r1tskina  10877  addcanpi  10994  mulcanpi  10995  elnpi  11083  addcan  11504  addcan2  11505  neg11  11619  negreb  11633  add20  11838  mulcand  11959  cru  12322  nn0lt10b  12771  uz11  13000  eqreznegel  13071  lbzbi  13073  rpnnen1lem6  13120  xrmaxlt  13321  xrltmin  13322  xrmaxle  13323  xrlemin  13324  xneg11  13355  xnn0xadd0  13387  xsubge0  13401  xrub  13452  elioc2  13550  elico2  13551  elicc2  13552  fzopth  13705  2ffzeq  13793  fzoopth  13907  flidz  13960  addmodlteq  14099  expeq0  14245  sq01  14379  fz1eqb  14508  hashen1  14524  hash1snb  14574  hashle2pr  14632  wrdnval  14700  eqwrd  14712  ccatalpha  14750  wrdl1s1  14773  ccats1alpha  14778  ccatopth  14876  ccatopth2  14877  wrdlen2  15107  cj11  15341  sqrt0  15420  abs00  15468  recan  15516  cnsqrt00  15572  rlimdm  15730  rpnnen2lem12  16405  0dvds  16458  dvds1  16501  alzdvds  16502  nn0enne  16559  nn0oddm1d2  16567  nnoddm1d2  16568  gcdeq0  16701  algcvgblem  16764  2mulprm  16880  prmexpb  16907  prmreclem3  17108  4sqlem11  17145  moni  17923  chnfibg  18822  grprcan  19196  grplcan  19223  grpinv11  19230  galcan  19530  sylow2a  19845  subgdisjb  19919  0ringdif  20790  domnlcanb  20983  domnrcanb  20985  drngmuleq0  21032  fidomndrng  21043  lspsncmp  21406  xrsdsreclb  21732  znidomb  21879  lmisfree  22160  coe1tm  22604  tgdom  23308  en1top  23314  cmpfi  23738  txcmpb  23975  hmeocnvb  24105  flimcls  24316  hauspwpwf1  24318  flftg  24327  ghmcnp  24446  metrest  24855  icoopnst  25272  iocopnst  25273  ishl2  25703  vitali  25946  mbfi1fseqlem4  26051  aannenlem1  26667  perfect  27570  2lgsoddprmlem3  27753  2sq2  27772  ltsval2  28025  bday0b  28211  negs11  28447  elnns2  28739  n0cutlt  28757  umgrislfupgrlem  29712  lfuhgr  29738  lfuhgr2  29739  usgrausgrb  29762  upgriswlk  30233  uhgrwkspth  30353  usgr2wlkspth  30357  usgr2trlspth  30359  usgr2pthspth  30360  extwwlkfab  30965  grporcan  31132  grpolcan  31144  ip2eqi  31470  hial2eq  31720  eigorthi  32451  stge1i  32852  stle0i  32853  mdbr3  32911  mdbr4  32912  atsseq  32961  mdsymlem7  33023  reuxfrdf  33141  disjunsn  33242  fpwrelmapffslem  33377  xmulcand  33540  prsdm  34599  prsrn  34600  infinfnum  35828  maxssj0  35960  mthmpps  36468  untangtr  36606  filnetlem4  37296  ordtopconn  37354  ordtopt0  37357  bj-dfbi6  37572  bj-spvew  37662  bj-19.9htbi  37732  relssresv  38093  bj-axseprep  38129  bj-elid6  38231  icorempo  38414  inunissunidif  38438  fvineqsneu  38474  wl-lem-moexsb  38640  seqpo  38821  qmapeldisjsbi  39933  lshpcmp  40185  lsatcmp  40200  lsatcmp2  40201  ltrneq2  41345  ltrneq  41346  tendospcanN  42220  dochlkr  42582  lcfl7N  42698  hgmap11  43099  ccatcan2d  43442  remulcan2d  43447  itrere  43515  log11d  43537  resubcan2  43579  readdcan2  43604  sn-addcand  43611  sn-addcan2d  43613  remulcand  43630  sn-itrere  43692  sn-retire  43693  cnreeu  43694  fphpd  43963  pellexlem3  43978  qirropth  44055  expdioph  44170  rpnnen3  44179  iotasbc  45542  cocanss2  46061  f1ocof1ob2  48291  2reu3  48320  rlimdmafv  48386  afv2orxorb  48437  rlimdmafv2  48467  funop1  48492  2ffzoeq  48537  prprelprb  48738  poprelb  48745  evenprm2  48951  perfectALTV  48960  nnsum3primesle9  49031  upgrwlkupwlkb  49378  islinindfis  49700  lincresunit3lem3  49725  blen1b  49839  line2ylem  50002  line2xlem  50004  line2y  50006  intubeu  50237  unilbeu  50238  thincn0eu  50705