Theorem impbid2 225

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

Ref	Expression
impbid2.1	⊢ (𝜓 → 𝜒)
impbid2.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
2		impbid2.1	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	impbid1 224	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 222	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimt  360  bimsc1  843  biorf  935  pm4.72  948  19.38a  1835  19.38b  1836  ax13b  2028  19.3t  2190  cgsexg  3515  cgsex2g  3516  cgsex4g  3517  cgsex4gOLD  3518  cgsex4gOLDOLD  3519  elab3gf  3672  elab3g  3673  abidnf  3696  reuan  3887  sscon34b  4290  elsn2g  4662  eqoreldif  4684  difsn  4797  elpreqprb  4864  dfnfc2  4927  intmin4  4975  dfiin2g  5029  elpw2g  5340  ssrel  5778  ssrelOLD  5779  ssrel2  5781  ssrelrel  5792  dmopab2rex  5914  releldmb  5942  relelrnb  5943  cnveqb  6194  dmsnopg  6211  relcnvtrg  6264  elsnxp  6289  onelssex  6411  ord0eln0  6418  f1ocnvb  6846  eqfnun  7040  ffvresb  7129  isof1oopb  7327  soisores  7329  riotaclb  7412  fnoprabg  7537  difex2  7756  dfwe2  7770  ordpwsuc  7812  ordunisuc2  7842  limsssuc  7848  dfom2  7866  relcnvexb  7928  dfsmo2  8361  ord1eln01  8510  ord2eln012  8511  omord  8582  nneob  8670  fsetcdmex  8875  pw2f1olem  9094  sucdom  9253  sucdomOLD  9254  1sdom  9266  fundmfibi  9349  f1dmvrnfibi  9354  fieq0  9438  hartogslem1  9559  rankr1ag  9819  rankeq0b  9877  fidomtri  10010  fidomtri2  10011  pr2ne  10021  isfin2-2  10336  enfin2i  10338  isfin3-2  10384  isf34lem6  10397  isfin1-2  10402  isfin1-3  10403  isfin7-2  10413  axgroth6  10845  ltsonq  10986  ltexnq  10992  znegclb  12623  rpneg  13032  nltpnft  13169  ngtmnft  13171  xrrebnd  13173  qextlt  13208  qextle  13209  iccneg  13475  fzsn  13569  fz1sbc  13603  fzofzp1b  13756  ceilidz  13843  fleqceilz  13845  hashclb  14343  hashnncl  14351  hashfun  14422  reim0b  15092  rexanre  15319  rexuzre  15325  lo1resb  15534  o1resb  15536  dvdsext  16291  zob  16329  ncoprmgcdne1b  16614  pceq0  16833  pc11  16842  pcz  16843  ramtcl  16972  cshwsiun  17062  oduposb  18314  pospo  18330  cnvpsb  18564  tsrlemax  18571  issubg2  19089  issubg4  19093  eqg0subg  19144  ghmmhmb  19174  pmtrmvd  19404  mndodcong  19490  issubrng2  20488  issubrg2  20524  ring2idlqusb  21193  lpigen  21218  cyggic  21499  ip2eq  21578  maducoeval2  22535  eltg3  22858  bastop  22877  0top  22879  iscld3  22961  isclo2  22985  cnprest  23186  dfconn2  23316  comppfsc  23429  cmphaushmeo  23697  reghaus  23722  nrmhaus  23723  fbun  23737  fsubbas  23764  ufileu  23816  uffix  23818  txflf  23903  fclsrest  23921  flimfnfcls  23925  ptcmplem2  23950  tgpt1  24015  tgpt0  24016  isngp2  24499  nrgdomn  24581  nmhmcn  25040  iscmet3  25214  limcflf  25803  ply1nzb  26051  coe11  26180  dgreq0  26193  eldmgm  26947  sqf11  27064  sqff1o  27107  zabsle1  27222  lgsabs1  27262  lgsquadlem2  27307  madebday  27819  oldbday  27820  slelss  27827  issubgr2  29078  uhgrissubgr  29081  usgrfilem  29133  uvtxnbgrb  29207  nbusgrvtxm1uvtx  29211  cusgrfilem3  29264  vdiscusgr  29338  wwlksn0s  29665  clwwlknon1loop  29901  clwwlknun  29915  nmobndi  30578  hmopadj2  31744  mdslle1i  32120  mdslle2i  32121  relfi  32385  ssrelf  32398  prodindf  33636  bnj1173  34627  revwlkb  34729  resconn  34850  cvmsval  34870  fmlafvel  34989  dmopab3rexdif  35009  elmrsubrn  35124  funsseq  35357  brcolinear  35649  outsideofeu  35721  lineunray  35737  nn0prpw  35801  bj-nfimexal  36096  bj-sngltag  36456  bj-elpwg  36525  bj-elsn0  36628  bj-opelid  36629  bj-opelidres  36634  bj-ideqg1  36637  bj-imdirval3  36657  bj-inftyexpiinj  36682  wl-ax11-lem2  37047  poimirlem26  37113  poimirlem27  37114  heicant  37122  cover2  37182  isbndx  37249  isbnd2  37250  equivbnd2  37259  prdsbnd2  37262  elghomlem2OLD  37353  isdrngo3  37426  riotaclbgBAD  38420  lssatle  38481  opcon3b  38662  cdlemk33N  40376  cdlemk34  40377  ioin9i8  41689  wepwsolem  42460  onsupmaxb  42661  rp-fakeimass  42936  iscard5  42960  cnvssb  43010  intimag  43080  ntrneiiso  43515  pm11.71  43828  pm14.122b  43854  pm14.123b  43857  iotavalb  43861  elixpconstg  44449  eliuniin  44459  eliuniin2  44480  climreeq  44995  f1cof1b  46451  rexrsb  46474  afv0nbfvbi  46525  dfafn5b  46535  elfz2z  46689  zeo2ALTV  47005  fpprwpprb  47074  nnlog2ge0lt1  47633

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »