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

Theorem mpbiri 167
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbiri.min 𝜒
mpbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbiri (𝜑𝜓)

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3 𝜒
21a1i 9 . 2 (𝜑𝜒)
3 mpbiri.maj . 2 (𝜑 → (𝜓𝜒))
42, 3mpbird 166 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.18im  1364  dedhb  2856  sbceqal  2967  ssdifeq0  3449  pwidg  3528  elpr2  3553  snidg  3560  exsnrex  3572  rabrsndc  3598  prid1g  3634  tpid1g  3642  tpid2g  3644  sssnr  3687  ssprr  3690  sstpr  3691  preqr1  3702  unimax  3777  intmin3  3805  eqbrtrdi  3974  pwnss  4090  0inp0  4097  bnd2  4104  exmid01  4128  exmidsssn  4132  exmidundif  4136  exmidundifim  4137  euabex  4154  copsexg  4173  euotd  4183  elopab  4187  epelg  4219  sucidg  4345  regexmidlem1  4455  sucprcreg  4471  onprc  4474  dtruex  4481  omelon2  4528  elvvuni  4610  eqrelriv  4639  relopabi  4672  opabid2  4677  ididg  4699  iss  4872  funopg  5164  fn0  5249  f00  5321  f0bi  5322  f1o00  5409  fo00  5410  brprcneu  5421  relelfvdm  5460  fsn  5599  eufnfv  5655  f1eqcocnv  5699  riotaprop  5760  acexmidlemb  5773  acexmidlemab  5775  acexmidlem2  5778  oprabid  5810  elrnmpo  5891  ov6g  5915  eqop2  6083  1stconst  6125  2ndconst  6126  dftpos3  6166  dftpos4  6167  2pwuninelg  6187  frecabcl  6303  ecopover  6534  map0g  6589  mapsn  6591  elixpsn  6636  en0  6696  en1  6700  fiprc  6716  dom0  6739  nneneq  6758  findcard  6789  findcard2  6790  findcard2s  6791  sbthlem2  6853  sbthlemi4  6855  sbthlemi5  6856  eldju2ndl  6964  updjudhf  6971  enumct  7007  fodjuomnilemdc  7023  nnnninf  7030  exmidonfinlem  7065  exmidaclem  7080  1ne0sr  7597  00sr  7600  cnm  7663  eqlei2  7881  divcanap3  8481  sup3exmid  8738  nn1suc  8762  nn0ge0  9025  xnn0xr  9068  xnn0nemnf  9074  elnn0z  9090  nn0n0n1ge2b  9153  nn0ind-raph  9191  elnn1uz2  9427  indstr2  9429  xrnemnf  9593  xrnepnf  9594  mnfltxr  9601  nn0pnfge0  9606  xrlttr  9610  xrltso  9611  xrlttri3  9612  nltpnft  9626  npnflt  9627  ngtmnft  9629  nmnfgt  9630  xsubge0  9693  xposdif  9694  xleaddadd  9699  fztpval  9893  fseq1p1m1  9904  fz01or  9921  qbtwnxr  10065  fzfig  10233  uzsinds  10245  ser0f  10318  1exp  10352  0exp  10358  bcn1  10535  zfz1iso  10615  sqrt0rlem  10806  prodf1f  11343  0dvds  11547  nn0o  11638  flodddiv4  11665  gcddvds  11686  bezoutlemmain  11720  lcmdvds  11794  rpdvds  11814  1nprm  11829  prmind2  11835  ennnfonelemj0  11948  ennnfonelemhf1o  11960  strslfv  12040  restsspw  12167  baspartn  12254  eltg3  12263  topnex  12292  discld  12342  lmreltop  12399  cnpfval  12401  cnprcl2k  12412  idcn  12418  xmet0  12569  blfvalps  12591  blfps  12615  blf  12616  limcimolemlt  12839  recnprss  12862  bj-om  13304  bj-nn0suc0  13317  bj-nn0suc  13331  bj-nn0sucALT  13345  bj-findis  13346  el2oss1o  13357  nninfall  13377  trilpolemcl  13403  dcapncf  13421
  Copyright terms: Public domain W3C validator