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 763  rgen2a 1691  dedhb 1906  dedth 2373  dedth2v 2374  dedth3v 2375  dedth4v 2376  elpr2 2415  ifpr 2417  snidg 2423  pri1gOLD 2440  pwpw0 2460  snsspr 2461  sssn 2464  sspr 2466  preqr1 2472  unimax 2522  intmin3 2548  syl6eqbr 2642  axsep2 2694  intabs 2723  0inp0 2728  snex 2740  opth1 2776  copsexg 2782  opprc3 2787  opth1gOLD 2788  elopab 2800  unisn2 2866  euuni 2871  reucl 2875  reuuni3 2876  onprc 2979  ordeleqon 2980  onint0 2997  ord0eln0 3013  nsuceq0 3043  0elsuc 3082  onuninsuc 3098  onun 3100  orduninsuc 3104  ordzsl 3106  onzsl 3107  limomss 3127  limom 3136  peano5 3143  tfinds 3151  elvvuni 3219  0nelxp 3230  opabid2 3257  issetid 3269  iss 3381  dmxpss 3459  rnxpss 3460  xpexr 3465  dfrel2 3471  coi1 3496  funopg 3533  fn0 3591  f00 3642  fconst 3643  f1o00 3699  fo00 3700  fnopabfv 3743  fsn 3819  fvi 3827  fconstfv 3834  canth 3892  tfrlem6 3901  oprabval3 4015  oprabval6g 4017  caoprmo 4056  2ndconst 4081  oawordeulem 4172  omwordi 4186  omwordri 4187  oaabs 4236  ecopoprdm 4293  map0e 4326  map0 4328  mapsn 4329  en0 4404  en1 4407  pw2en 4426  sbthlem2 4428  sbthlem4 4430  sbthlem5 4431  fodomr 4463  mapxpen 4475  xpmapenlem5 4480  nneneq 4492  php3 4495  fodomfi 4540  supub 4554  suplub 4555  sucprcreg 4572  inf3lemd 4584  inf3lem6 4590  noinfep 4612  trcl 4617  r1tr 4626  r1val1 4630  rankr1 4646  scottex 4688  scott0 4689  bnd2 4696  ac6lem 4726  numth2 4757  cardval 4798  oncard 4801  cardidm 4821  cardlim 4823  ondomon 4828  cardprc 4833  cardaleph 4857  cfub 4880  cflecard 4884  cfle 4885  cfsuc 4887  axpowndlem3 4923  indpi 5006  distrpqlem 5038  1pr 5089  ltsopr 5108  prlem934b 5110  recexpr 5132  1ne0sr 5177  0idsr 5178  00sr 5180  recexsrlem 5184  leidt 5504  pnfnemnf 5509  mnfltxrt 5518  xrlttrit 5525  xrlttrt 5526  xrleidt 5533  lelttrit 5596  lemul1it 5793  lemul1itOLD 5794  posex 5856  nn1suc 5887  xrub 6027  nn0subt 6108  zltp1let 6128  nn0ind-raph 6162  elq 6195  qbtwnxr 6217  shftfn 6280  limsupclt 6462  seqzfn 6471  seqzres 6492  seqzres2 6493  expne0it 6519  0expt 6521  expwordit 6534  sqr0 6602  sqrlem6 6608  sqrmsq 6639  sqr2irrlem1 6654  replimt 6692  recvalz 6825  abs1m 6841  faclbnd4lem1 6885  mulc1cncf 7214  ruclem36 7488  infxpidmlem7 7501  infmap2 7523  eltg3t 7568  islp2 7688  qdensere 7691  cnsscnp 7711  met0 7754  blf 7784  lmrel 7865  subgrnss 8056  ringsn 8100  nvmid 8225  ubthlem8 8467  efifolem6 8642  hiidrclt 8882  hsn0elch 9041  ocsh 9072  hsupunss 9228  spanss2 9229  shjshsel 9331  cmbr4 9461  dfiop2 9596  kbpjt 9796  nmopunt 9854  adjbdlnt 9931  pjssdif1 10014  pjinvar 10029  pjcmmul2 10040  pj3 10046  stge1 10075  stle0 10076  mdsym 10246  sumdmdlem2 10253  dmdbr6at 10256  stcat 10353  ump 10355  abfi2 10378  hmeogrp 10425  emhgrat 10611

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