ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbiri Unicode 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  |-  ch
mpbiri.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbiri  |-  ( ph  ->  ps )

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3  |-  ch
21a1i 9 . 2  |-  ( ph  ->  ch )
3 mpbiri.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbird 166 1  |-  ( ph  ->  ps )
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  8425  sup3exmid  8679  nn1suc  8703  nn0ge0  8960  xnn0xr  9003  xnn0nemnf  9009  elnn0z  9025  nn0n0n1ge2b  9088  nn0ind-raph  9126  elnn1uz2  9357  indstr2  9359  xrnemnf  9519  xrnepnf  9520  mnfltxr  9527  nn0pnfge0  9532  xrlttr  9536  xrltso  9537  xrlttri3  9538  nltpnft  9552  npnflt  9553  ngtmnft  9555  nmnfgt  9556  xsubge0  9619  xposdif  9620  xleaddadd  9625  fztpval  9818  fseq1p1m1  9829  fz01or  9846  qbtwnxr  9990  fzfig  10158  uzsinds  10170  ser0f  10243  1exp  10277  0exp  10283  bcn1  10459  zfz1iso  10539  sqrt0rlem  10730  0dvds  11425  nn0o  11516  flodddiv4  11543  gcddvds  11564  bezoutlemmain  11598  lcmdvds  11672  rpdvds  11692  1nprm  11707  prmind2  11713  ennnfonelemj0  11825  ennnfonelemhf1o  11837  strslfv  11914  restsspw  12041  baspartn  12128  eltg3  12137  topnex  12166  discld  12216  lmreltop  12273  cnpfval  12275  cnprcl2k  12286  idcn  12292  xmet0  12443  blfvalps  12465  blfps  12489  blf  12490  limcimolemlt  12713  recnprss  12736  bj-om  13031  bj-nn0suc0  13044  bj-nn0suc  13058  bj-nn0sucALT  13072  bj-findis  13073  el2oss1o  13084  nninfall  13100  trilpolemcl  13126
  Copyright terms: Public domain W3C validator