ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impbid GIF version

Theorem impbid 120
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1 (𝜑 → (𝜓𝜒))
impbid.2 (𝜑 → (𝜒𝜓))
Assertion
Ref Expression
impbid (𝜑 → (𝜓𝜒))

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3 (𝜑 → (𝜓𝜒))
2 impbid.2 . . 3 (𝜑 → (𝜒𝜓))
31, 2impbid21d 119 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 43 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bicom1  122  impbid1  130  pm5.74  168  imbi1d  220  pm5.501  233  pm5.32d  423  impbida  528  notbid  592  pm5.21  611  nbn2  613  2falsed  618  pm5.21ndd  621  orbi2d  704  con4biddc  754  con1bidc  768  con1bdc  772  oibabs  800  dedlema  876  dedlemb  877  xorbin  1275  albi  1357  19.21ht  1473  exbi  1495  19.23t  1567  equequ1  1598  equequ2  1599  elequ1  1600  elequ2  1601  equsexd  1617  dral1  1618  cbv2h  1634  sbequ12  1654  sbiedh  1670  drex1  1679  ax11b  1707  sbequ  1721  sbft  1728  sb56  1765  cbvexdh  1801  eupickb  1981  eupickbi  1982  ceqsalt  2580  ceqex  2671  mob2  2721  euxfr2dc  2726  reu6  2730  sbciegft  2793  eqsbc3r  2819  csbiebt  2886  sseq1  2966  reupick  3221  reupick2  3223  disjeq2  3749  disjeq1  3752  copsexg  3981  euotd  3991  poeq2  4037  sotritric  4061  sotritrieq  4062  seeq1  4076  seeq2  4077  alxfr  4193  ralxfrd  4194  rexxfrd  4195  ordelsuc  4231  sosng  4413  iss  4654  iotaval  4878  funeq  4921  funssres  4942  tz6.12c  5203  fnbrfvb  5214  ssimaex  5234  fvimacnv  5282  elpreima  5286  fsn  5335  fconst2g  5376  elunirn  5405  f1ocnvfvb  5420  foeqcnvco  5430  f1eqcocnv  5431  fliftfun  5436  isose  5460  isopo  5462  isoso  5464  f1oiso2  5466  eusvobj2  5498  oprabid  5537  f1opw2  5706  op1steq  5805  rntpos  5872  nnsucelsuc  6070  nnsucsssuc  6071  nnsseleq  6079  nnaord  6082  nnmord  6090  nnaordex  6100  nnawordex  6101  nnm00  6102  erexb  6131  swoord1  6135  swoord2  6136  iinerm  6178  fundmen  6286  nneneq  6320  nndomo  6326  fidifsnen  6331  ordiso2  6355  ordiso  6356  ltexnqq  6504  genprndl  6617  genprndu  6618  nqprl  6647  nqpru  6648  1idprl  6686  1idpru  6687  ltexprlemrnd  6701  ltaprg  6715  recexprlemrnd  6725  cauappcvgprlemrnd  6746  caucvgprlemrnd  6769  caucvgprprlemrnd  6797  ltxrlt  7083  lttri3  7096  ltadd2  7414  reapti  7568  apreap  7576  ltmul1  7581  apreim  7592  ltleap  7619  mulap0b  7634  apmul1  7762  lt2msq  7850  nnsub  7950  zltnle  8289  zleloe  8290  zrevaddcl  8293  zltp1le  8296  zapne  8313  nn0n0n1ge2b  8318  zdiv  8326  nneo  8339  zeo2  8342  qrevaddcl  8576  xltneg  8747  iccid  8792  fzn  8904  0fz1  8907  uzsplit  8952  fzm1  8960  fzrevral  8965  ssfzo12bi  9079  qltnle  9099  flqge  9122  frec2uzlt2d  9188  shftlem  9415  shftuz  9416  caucvgrelemcau  9577  sqrtsq  9640  abs00ap  9658  cau3lem  9708  climshft  9823  bj-notbi  10043
  Copyright terms: Public domain W3C validator