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  1348  dedhb  2826  sbceqal  2936  ssdifeq0  3415  pwidg  3494  elpr2  3519  snidg  3524  exsnrex  3536  rabrsndc  3561  prid1g  3597  tpid1g  3605  tpid2g  3607  sssnr  3650  ssprr  3653  sstpr  3654  preqr1  3665  unimax  3740  intmin3  3768  eqbrtrdi  3937  pwnss  4053  0inp0  4060  bnd2  4067  exmid01  4091  exmidsssn  4095  exmidundif  4099  exmidundifim  4100  euabex  4117  copsexg  4136  euotd  4146  elopab  4150  epelg  4182  sucidg  4308  regexmidlem1  4418  sucprcreg  4434  onprc  4437  dtruex  4444  omelon2  4491  elvvuni  4573  eqrelriv  4602  relopabi  4635  opabid2  4640  ididg  4662  iss  4835  funopg  5127  fn0  5212  f00  5284  f0bi  5285  f1o00  5370  fo00  5371  brprcneu  5382  relelfvdm  5421  fsn  5560  eufnfv  5616  f1eqcocnv  5660  riotaprop  5721  acexmidlemb  5734  acexmidlemab  5736  acexmidlem2  5739  oprabid  5771  elrnmpo  5852  ov6g  5876  eqop2  6044  1stconst  6086  2ndconst  6087  dftpos3  6127  dftpos4  6128  2pwuninelg  6148  frecabcl  6264  ecopover  6495  map0g  6550  mapsn  6552  elixpsn  6597  en0  6657  en1  6661  fiprc  6677  dom0  6700  nneneq  6719  findcard  6750  findcard2  6751  findcard2s  6752  sbthlem2  6814  sbthlemi4  6816  sbthlemi5  6817  eldju2ndl  6925  updjudhf  6932  enumct  6968  fodjuomnilemdc  6984  nnnninf  6991  exmidonfinlem  7017  exmidaclem  7032  1ne0sr  7542  00sr  7545  cnm  7608  eqlei2  7826  divcanap3  8426  sup3exmid  8683  nn1suc  8707  nn0ge0  8970  xnn0xr  9013  xnn0nemnf  9019  elnn0z  9035  nn0n0n1ge2b  9098  nn0ind-raph  9136  elnn1uz2  9369  indstr2  9371  xrnemnf  9532  xrnepnf  9533  mnfltxr  9540  nn0pnfge0  9545  xrlttr  9549  xrltso  9550  xrlttri3  9551  nltpnft  9565  npnflt  9566  ngtmnft  9568  nmnfgt  9569  xsubge0  9632  xposdif  9633  xleaddadd  9638  fztpval  9831  fseq1p1m1  9842  fz01or  9859  qbtwnxr  10003  fzfig  10171  uzsinds  10183  ser0f  10256  1exp  10290  0exp  10296  bcn1  10472  zfz1iso  10552  sqrt0rlem  10743  0dvds  11440  nn0o  11531  flodddiv4  11558  gcddvds  11579  bezoutlemmain  11613  lcmdvds  11687  rpdvds  11707  1nprm  11722  prmind2  11728  ennnfonelemj0  11841  ennnfonelemhf1o  11853  strslfv  11930  restsspw  12057  baspartn  12144  eltg3  12153  topnex  12182  discld  12232  lmreltop  12289  cnpfval  12291  cnprcl2k  12302  idcn  12308  xmet0  12459  blfvalps  12481  blfps  12505  blf  12506  limcimolemlt  12729  recnprss  12752  bj-om  13062  bj-nn0suc0  13075  bj-nn0suc  13089  bj-nn0sucALT  13103  bj-findis  13104  el2oss1o  13115  nninfall  13131  trilpolemcl  13157
  Copyright terms: Public domain W3C validator