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  1346  dedhb  2824  sbceqal  2934  ssdifeq0  3413  pwidg  3492  elpr2  3517  snidg  3522  exsnrex  3534  rabrsndc  3559  prid1g  3595  tpid1g  3603  tpid2g  3605  sssnr  3648  ssprr  3651  sstpr  3652  preqr1  3663  unimax  3738  intmin3  3766  eqbrtrdi  3935  pwnss  4051  0inp0  4058  bnd2  4065  exmid01  4089  exmidsssn  4093  exmidundif  4097  exmidundifim  4098  euabex  4115  copsexg  4134  euotd  4144  elopab  4148  epelg  4180  sucidg  4306  regexmidlem1  4416  sucprcreg  4432  onprc  4435  dtruex  4442  omelon2  4489  elvvuni  4571  eqrelriv  4600  relopabi  4633  opabid2  4638  ididg  4660  iss  4833  funopg  5125  fn0  5210  f00  5282  f0bi  5283  f1o00  5368  fo00  5369  brprcneu  5380  relelfvdm  5419  fsn  5558  eufnfv  5614  f1eqcocnv  5658  riotaprop  5719  acexmidlemb  5732  acexmidlemab  5734  acexmidlem2  5737  oprabid  5769  elrnmpo  5850  ov6g  5874  eqop2  6042  1stconst  6084  2ndconst  6085  dftpos3  6125  dftpos4  6126  2pwuninelg  6146  frecabcl  6262  ecopover  6493  map0g  6548  mapsn  6550  elixpsn  6595  en0  6655  en1  6659  fiprc  6675  dom0  6698  nneneq  6717  findcard  6748  findcard2  6749  findcard2s  6750  sbthlem2  6812  sbthlemi4  6814  sbthlemi5  6815  eldju2ndl  6923  updjudhf  6930  enumct  6966  fodjuomnilemdc  6982  nnnninf  6989  exmidaclem  7028  1ne0sr  7538  00sr  7541  cnm  7604  eqlei2  7822  divcanap3  8418  sup3exmid  8672  nn1suc  8696  nn0ge0  8953  xnn0xr  8996  xnn0nemnf  9002  elnn0z  9018  nn0n0n1ge2b  9081  nn0ind-raph  9119  elnn1uz2  9350  indstr2  9352  xrnemnf  9504  xrnepnf  9505  mnfltxr  9512  nn0pnfge0  9517  xrlttr  9521  xrltso  9522  xrlttri3  9523  nltpnft  9537  npnflt  9538  ngtmnft  9540  nmnfgt  9541  xsubge0  9604  xposdif  9605  xleaddadd  9610  fztpval  9803  fseq1p1m1  9814  fz01or  9831  qbtwnxr  9975  fzfig  10143  uzsinds  10155  ser0f  10228  1exp  10262  0exp  10268  bcn1  10444  zfz1iso  10524  sqrt0rlem  10715  0dvds  11409  nn0o  11500  flodddiv4  11527  gcddvds  11548  bezoutlemmain  11582  lcmdvds  11656  rpdvds  11676  1nprm  11691  prmind2  11697  ennnfonelemj0  11809  ennnfonelemhf1o  11821  strslfv  11898  restsspw  12025  baspartn  12112  eltg3  12121  topnex  12150  discld  12200  lmreltop  12257  cnpfval  12259  cnprcl2k  12270  idcn  12276  xmet0  12427  blfvalps  12449  blfps  12473  blf  12474  limcimolemlt  12676  recnprss  12699  bj-om  12937  bj-nn0suc0  12950  bj-nn0suc  12964  bj-nn0sucALT  12978  bj-findis  12979  el2oss1o  12990  nninfall  13006  trilpolemcl  13032
  Copyright terms: Public domain W3C validator