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 765  rgen2a 1699  dedhb 1915  dedth 2383  dedth2v 2384  dedth3v 2385  dedth4v 2386  elpr2 2425  ifpr 2427  snidg 2433  pwpw0 2469  snsspr 2470  sssn 2473  sspr 2475  preqr1 2481  pwsnALT 2501  unimax 2532  intmin3 2558  syl6eqbr 2652  axsep2 2704  intabs 2733  0inp0 2738  snex 2750  opth1 2786  copsexg 2792  opprc3 2797  elopab 2811  unisn2 2875  euuni 2881  reucl 2885  reuuni3 2886  onprc 2989  ordeleqon 2990  onint0 3007  ord0eln0 3023  nsuceq0 3053  0elsuc 3092  onuninsuc 3108  onun 3110  orduninsuc 3114  ordzsl 3116  onzsl 3117  limomss 3137  limom 3146  peano5 3153  tfinds 3161  elvvuni 3229  0nelxp 3240  opabid2 3267  issetid 3280  iss 3397  dmxpss 3473  rnxpss 3474  xpexr 3479  dfrel2 3485  coi1 3510  funopg 3547  fn0 3605  f00 3657  fconst 3658  f1o00 3714  fo00 3715  fnopabfv 3758  fsn 3834  fvi 3842  fconstfv 3849  canth 3907  tfrlem6 3916  oprabval3 4030  oprabval6g 4032  caoprmo 4070  2ndconst 4097  oawordeulem 4188  omwordi 4202  omwordri 4203  oaabs 4252  ecopoprdm 4309  map0e 4342  map0 4344  mapsn 4345  en0 4423  en1 4426  pw2en 4446  sbthlem2 4448  sbthlem4 4450  sbthlem5 4451  fodomr 4483  mapxpen 4495  xpmapenlem5 4500  nneneq 4512  php3 4515  php3OLD 4516  fodomfiOLD 4566  supub 4580  suplub 4581  sucprcreg 4600  inf3lemd 4612  inf3lem6 4618  noinfep 4640  trcl 4645  r1tr 4654  r1val1 4658  rankr1 4674  scottex 4716  scott0 4717  bnd2 4724  ac6lem 4754  numth2 4785  cardval 4826  oncard 4829  cardidm 4849  cardlim 4851  ondomon 4856  cardprc 4861  cardaleph 4885  cfub 4908  cflecard 4912  cfle 4913  cfsuc 4915  axpowndlem3 4951  indpi 5034  distrpqlem 5066  1pr 5117  ltsopr 5136  prlem934b 5138  recexpr 5160  1ne0sr 5205  0idsr 5206  00sr 5208  recexsrlem 5212  leidt 5531  pnfnemnf 5536  mnfltxrt 5545  xrlttrit 5552  xrlttrt 5553  xrleidt 5560  lelttrit 5622  lemul1it 5837  lemul1itOLD 5838  posex 5908  nn1suc 5939  xrub 6080  nn0subt 6161  zltp1let 6181  nn0ind-raph 6214  elq 6257  qbtwnxr 6279  shftfn 6343  limsupclt 6530  seqzfn 6539  seqzres 6560  seqzres2 6561  expne0it 6588  0expt 6590  expwordit 6603  sqr0 6672  sqrlem6 6678  sqrmsq 6709  sqr2irrlem1 6724  replimt 6761  recvalz 6887  abs1m 6904  faclbnd4lem1 6948  mulc1cncf 7279  efcltlem1 7304  ruclem36 7545  infxpidmlem7 7558  infmap2 7581  eltg3t 7626  islp2 7747  qdensere 7751  cnsscnp 7772  met0 7815  metne0 7821  blf 7844  lmrel 7927  subgrnss 8119  ringsn 8163  nvmid 8285  ubthlem8 8536  efifolem6 8727  hiidrclt 8961  hsn0elch 9120  ocsh 9156  hsupunss 9313  spanss2 9314  shjshsel 9416  cmbr4 9544  dfiop2 9679  kbpjt 9880  nmopunt 9939  adjbdlnt 10016  adjeq0 10024  pjssdif1 10103  pjinvar 10119  pjcmmul2 10130  pj3 10136  stge1 10165  stle0 10166  mdsym 10338  sumdmdlem2 10346  dmdbr6at 10350  dmdbr7at 10351  stcat 10457  ump 10459  abfi2 10490  abfi2OLD 10491  hmeogrp 10538  top1 10547  top2ind 10548  rcfpfillem5 10593  rcfpfillem5OLD 10594  rcfpfil 10597  rcfpfilOLD 10598  emhgrat 10775

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