Theorem mpbiri 192

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 152	. 2 |- (ph -> (ch -> ps))
4	1, 3	mpi 44	1 |- (ph -> ps)

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

This theorem is referenced by:  dedt 770  rgen2a 1745  dedhb 1961  dedth 2437  dedth2vOLD 2438  dedth3vOLD 2439  dedth4vOLD 2440  elpr2 2483  ifpr 2485  snidg 2494  prid1g 2511  pwpw0 2533  snsspr1 2534  sssn 2538  sspr 2540  preqr1 2546  pwsnALT 2566  reucl 2584  unimax 2599  intmin3 2625  syl6eqbr 2725  axsep2 2778  intabs 2807  0inp0 2812  axpweq 2817  snex 2826  opth1 2862  copsexg 2868  opprc3 2873  elopab 2888  ord0eln0 3027  nsuceq0 3053  onun2i 3085  unisn2 3098  euuni 3105  reuuni3 3109  onprc 3143  ordeleqon 3144  onint0 3153  0elsuc 3189  onuninsuci 3194  orduninsuc 3197  ordzsl 3199  onzsl 3200  tfinds 3212  limomss 3224  limom 3233  peano5 3241  elvvuni 3315  0nelxp 3326  opabid2 3360  issetid 3370  iss 3487  dmxpss 3558  rnxpss 3559  xpexr 3564  dfrel2 3569  coi1 3614  funopg 3652  fn0 3711  f00 3764  fconst 3765  resdif 3816  f1o00 3825  fo00 3826  dffn5 3869  fsn 3948  fvi 3956  fconstfv 3963  oprabval3 4090  oprabval6g 4093  caoprmo 4131  1stconst 4190  2ndconst 4191  canth 4205  tfrlem6 4217  oawordeulem 4324  omwordi 4338  omwordri 4339  oaabs 4392  ecopoprdm 4450  map0e 4483  map0 4485  mapsn 4486  en0 4564  en1 4567  fiprc 4574  pw2en 4587  ac6sfi 4591  sbthlem2 4593  sbthlem4 4595  sbthlem5 4596  fodomr 4628  mapxpen 4642  xpmapenlem5 4647  nneneq 4659  php3 4662  fodomfi 4709  supub 4723  suplub 4724  sucprcreg 4743  inf3lemd 4757  inf3lem6 4763  noinfep 4786  trcl 4791  r1tr 4800  r1val1 4804  rankr1 4820  scottex 4862  scott0 4863  bnd2 4870  ac6lem 4900  numth2 4931  cardval 4973  oncard 4976  cardidm 4999  cardlim 5001  ondomon 5006  cardprc 5011  cardaleph 5035  cfub 5058  cflecard 5062  cfle 5063  cfsuc 5065  axpowndlem3 5105  indpi 5188  distrpqlem 5220  1pr 5271  ltsopr 5290  prlem934b 5292  recexpr 5314  1ne0sr 5359  0idsr 5360  00sr 5362  recexsrlem 5366  leid 5685  mnfltxr 5699  xrlttri 5706  xrlttr 5707  xrleid 5714  lelttric 5776  lemul1a 5981  lemul1aOLD 5982  posexi 6053  nn1suc 6084  xrub 6248  nn0sub 6329  zltp1le 6349  nn0ind-raph 6385  elq 6396  qbtwnxr 6419  shftfn 6708  limsupcl 6725  seqzfn 6734  seqzres 6755  seqzres2 6756  expne0i 6782  0exp 6784  expwordi 6800  sqr0 6873  sqrlem6 6879  sqrmsqi 6910  sqr2irrlem1 6925  replim 6962  recvalzi 7090  abs1mi 7107  faclbnd4lem1 7151  mulc1cncf 7484  efcltlem1 7509  egt2OLD 7600  egt2lt3 7602  ruclem36 7757  infxpidmlem7 7770  infmap2 7793  eltg3 7838  islp2 7957  qdensere 7961  cnsscnp 7982  met0 8025  metn0 8031  blf 8054  lmrel 8138  subgrnss 8361  ringsn 8405  nvmid 8532  ubthlem8 8794  efifolem6 8999  grothpw 9054  hiidrcl 9237  hsn0elch 9396  ocsh 9432  hsupunss 9589  spanss2 9590  shjshseli 9692  cmbr4i 9820  dfiop2 9959  kbpj 10160  nmopun 10218  adjbdln 10295  adjeq0 10303  pjssdif1i 10383  pjinvari 10400  pjcmmul2i 10411  pj3i 10417  stge1i 10446  stle0i 10447  mdsymi 10620  sumdmdlem2 10628  dmdbr6ati 10632  dmdbr7ati 10633  stcat 10741  ump 10743  scprefat 10783  scprefat2 10784  imfstnrelc 10810  set2elt 10827  setwoe 10828  abfi2 10853  inposet 10868  lteqtpos 10880  dispos 10881  ismgm 10897  isppm 10917  unmnd 10951  on1el4 10963  zrdivrng 10969  oibbi1 11004  oibbi2 11005  hmeogrp 11044  top1 11049  top2ind 11050  subspemp 11060  stoig 11064  rcfpfillem5 11093  rcfpfil 11095  bwt2 11123  clindistop 11131  extrdom 11236  extrcod 11237  extrcmp 11238  extrid 11239  catsbc 11303  r19.2zb 11393  elfiun 11421  hartog 11436  infenomsub 11450  elsubsp 11477  subcld 11480  subcls 11481  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  alexsublem2 11497  alexsublem3 11498  alexsub 11500  connsub 11502  subtopmetlem 11505  fneref 11554  refref 11555  neibastop2lem3 11582  neibastop2lem4 11583  topmeet 11587  topjoin 11588  fnejoin2 11592  fbssint 11626  filfinnfr 11646  ufileu 11658  fixufil 11661  filcon 11665  rnelfm 11699  fmfnfmlem2 11701  fcluscf 11724  flimfnfcls 11727  fcluscomp 11733  sfclusf 11736  dirref 11752  gapm 11784  upixp 11823  dif1en 11833  findcard 11836  fimax 11837  indexf 11847  inficl 11849  sdc 11877  cncfco 11948  piececn 11955  tx1cn 11976  tx2cn 11977  heiborlem6 12016  heiborlem13 12023  heiborlem18 12028  heiborlem21 12031  rrntotbnd 12078  phtpycolem2 12094  isphtpc2 12102  emhgrat 12201

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 145

Copyright terms: Public domain