Theorem mpbiri 194

Description: An inference from a nested biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbiri.min	|- ch
mpbiri.maj	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
mpbiri	|- (ph -> ps)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. 2 |- ch
2		mpbiri.maj	. . 3 |- (ph -> (ps <-> ch))
3	2	biimprd 154	. 2 |- (ph -> (ch -> ps))
4	1, 3	mpi 44	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  dedt 769  rgen2a 1706  dedhb 1922  dedth 2393  dedth2v 2394  dedth3v 2395  dedth4v 2396  elpr2 2435  ifpr 2437  snidg 2443  prid1g 2460  pwpw0 2481  snsspr 2482  sssn 2485  sspr 2487  preqr1 2493  pwsnALT 2513  unimax 2544  intmin3 2570  syl6eqbr 2665  axsep2 2717  intabs 2746  0inp0 2751  snex 2764  opth1 2800  copsexg 2806  opprc3 2811  elopab 2825  unisn2 2889  euuni 2895  reucl 2899  reuuni3 2900  onprc 3003  ordeleqon 3004  onint0 3021  ord0eln0 3037  nsuceq0 3067  0elsuc 3106  onuninsuc 3122  onun 3124  orduninsuc 3128  ordzsl 3130  onzsl 3131  limomss 3151  limom 3160  peano5 3167  tfinds 3175  elvvuni 3243  0nelxp 3254  opabid2 3281  issetid 3294  iss 3411  dmxpss 3487  rnxpss 3488  xpexr 3493  dfrel2 3499  coi1 3524  funopg 3561  fn0 3619  f00 3671  fconst 3672  f1o00 3728  fo00 3729  fnopabfv 3772  fsn 3848  fvi 3856  fconstfv 3863  canth 3921  tfrlem6 3930  oprabval3 4044  oprabval6g 4046  caoprmo 4084  2ndconst 4111  oawordeulem 4202  omwordi 4216  omwordri 4217  oaabs 4266  ecopoprdm 4323  map0e 4356  map0 4358  mapsn 4359  en0 4437  en1 4440  pw2en 4461  sbthlem2 4463  sbthlem4 4465  sbthlem5 4466  fodomr 4498  mapxpen 4510  xpmapenlem5 4515  nneneq 4527  php3 4530  fodomfi 4576  supub 4590  suplub 4591  sucprcreg 4610  inf3lemd 4624  inf3lem6 4630  noinfep 4652  trcl 4657  r1tr 4666  r1val1 4670  rankr1 4686  scottex 4728  scott0 4729  bnd2 4736  ac6lem 4766  numth2 4797  cardval 4838  oncard 4841  cardidm 4862  cardlim 4864  ondomon 4869  cardprc 4874  cardaleph 4898  cfub 4921  cflecard 4925  cfle 4926  cfsuc 4928  axpowndlem3 4964  indpi 5047  distrpqlem 5079  1pr 5130  ltsopr 5149  prlem934b 5151  recexpr 5173  1ne0sr 5218  0idsr 5219  00sr 5221  recexsrlem 5225  leidt 5544  pnfnemnf 5549  mnfltxrt 5558  xrlttrit 5565  xrlttrt 5566  xrleidt 5573  lelttrit 5635  lemul1it 5841  lemul1itOLD 5842  posex 5914  nn1suc 5945  xrub 6086  nn0subt 6167  zltp1let 6187  nn0ind-raph 6223  elq 6267  qbtwnxr 6290  shftfn 6526  limsupclt 6543  seqzfn 6552  seqzres 6573  seqzres2 6574  expne0it 6601  0expt 6603  expwordit 6616  sqr0 6686  sqrlem6 6692  sqrmsq 6723  sqr2irrlem1 6738  replimt 6775  recvalz 6901  abs1m 6918  faclbnd4lem1 6962  mulc1cncf 7293  efcltlem1 7318  ruclem36 7560  infxpidmlem7 7573  infmap2 7596  eltg3t 7638  islp2 7756  qdensere 7760  cnsscnp 7781  met0 7824  metne0 7830  blf 7853  lmrel 7936  subgrnss 8127  ringsn 8171  nvmid 8293  ubthlem8 8544  efifolem6 8734  hiidrclt 8968  hsn0elch 9127  ocsh 9163  hsupunss 9320  spanss2 9321  shjshsel 9423  cmbr4 9551  dfiop2 9686  kbpjt 9887  nmopunt 9946  adjbdlnt 10023  adjeq0 10031  pjssdif1 10110  pjinvar 10127  pjcmmul2 10138  pj3 10144  stge1 10173  stle0 10174  mdsym 10346  sumdmdlem2 10354  dmdbr6at 10358  dmdbr7at 10359  stcat 10460  ump 10462  abfi2 10493  inposet 10496  hmeogrp 10544  set2elt 10551  setwoe 10552  top1 10553  top2ind 10554  rcfpfillem5 10587  rcfpfil 10589  emhgrat 10767

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain