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

Theorem mpbiri 166
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 165 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.18im  1317  dedhb  2762  sbceqal  2870  ssdifeq0  3326  pwidg  3397  elpr2  3422  snidg  3425  exsnrex  3437  rabrsndc  3462  prid1g  3498  sssnr  3547  ssprr  3550  sstpr  3551  preqr1  3562  unimax  3637  intmin3  3665  syl6eqbr  3824  pwnss  3935  0inp0  3942  bnd2  3949  euabex  3982  copsexg  4001  euotd  4011  elopab  4015  epelg  4047  sucidg  4173  regexmidlem1  4278  sucprcreg  4294  onprc  4297  dtruex  4304  omelon2  4350  elvvuni  4424  eqrelriv  4453  relopabi  4485  opabid2  4489  ididg  4511  iss  4678  funopg  4958  fn0  5043  f00  5106  f1o00  5186  fo00  5187  brprcneu  5196  relelfvdm  5231  fsn  5361  eufnfv  5415  f1eqcocnv  5456  riotaprop  5516  acexmidlemb  5529  acexmidlemab  5531  acexmidlem2  5534  oprabid  5562  elrnmpt2  5639  ov6g  5663  eqop2  5829  1stconst  5867  2ndconst  5868  dftpos3  5905  dftpos4  5906  2pwuninelg  5926  frecabcl  6042  ecopover  6263  en0  6334  en1  6338  fiprc  6351  nneneq  6382  findcard  6412  findcard2  6413  findcard2s  6414  1ne0sr  6994  00sr  6997  eqlei2  7261  divcanap3  7842  nn1suc  8114  nn0ge0  8369  xnn0xr  8412  xnn0nemnf  8418  elnn0z  8434  nn0n0n1ge2b  8497  nn0ind-raph  8534  elnn1uz2  8764  indstr2  8766  xrnemnf  8918  xrnepnf  8919  mnfltxr  8926  nn0pnfge0  8931  xrlttr  8935  xrltso  8936  xrlttri3  8937  nltpnft  8949  ngtmnft  8950  fztpval  9165  fseq1p1m1  9176  fz01or  9193  qbtwnxr  9333  fzfig  9501  uzsinds  9507  iser0f  9558  1exp  9591  0exp  9597  bcn1  9771  sqrt0rlem  10016  0dvds  10349  nn0o  10440  flodddiv4  10467  gcddvds  10488  bezoutlemmain  10520  lcmdvds  10594  rpdvds  10614  1nprm  10629  prmind2  10635  bj-om  10875  bj-nn0suc0  10888  bj-nn0suc  10902  bj-nn0sucALT  10916  bj-findis  10917
  Copyright terms: Public domain W3C validator