Theorem mpbiri 211

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

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

This theorem is referenced by:  dedt 842  rgen2a 2160  rgen2aOLD 2161  dedhb 2426  sbceqal 2502  r19.2zb 2959  dedth 3011  dedth2vOLD 3012  dedth3vOLD 3013  dedth4vOLD 3014  elpr2 3062  snidg 3067  ifpr 3077  prid1g 3104  pwpw0 3134  snsspr1OLD 3136  sssn 3142  sspr 3144  preqr1 3152  pwsnALT 3173  unimax 3212  reucl 3213  unissint 3241  unissintOLD 3242  intmin3 3245  syl6eqbr 3374  axsep2 3439  intabs 3469  0inp0 3475  axpweq 3480  snexOLD 3493  opth1 3531  copsexg 3537  copsexgOLD 3538  opprc3 3543  elopab 3559  ord0eln0 3717  sucidg 3743  nsuceq0 3749  onun2i 3785  unisn2 3799  euuni 3807  reuuni3 3812  onprc 3865  ordeleqon 3866  onint0 3877  0elsuc 3916  onuninsuci 3921  orduninsuc 3925  ordzsl 3927  onzsl 3928  onzslOLD 3929  tfinds 3942  tfindsOLD 3943  limomss 3956  limom 3967  peano5 3975  elvvuni 4055  0nelxp 4066  opabid2 4107  ididg 4117  issetidOLD 4122  iss 4254  issOLD 4255  dmxpss 4343  rnxpssOLD 4345  xpexr 4352  dfrel2 4358  dmsnop 4367  coi1 4413  funopg 4454  fn0 4532  fn0OLD 4533  f00 4601  fconstOLD 4603  resdif 4659  f1o00 4668  fo00 4669  dffn5 4717  eufnfv 4771  fsn 4807  fvi 4818  fconstfv 4825  oprabval3 4959  oprabval6g 4962  caoprmo 5003  1stconst 5070  2ndconst 5071  canth 5112  tfrlem6 5124  oawordeulem 5236  omwordi 5250  omwordri 5251  oaabs 5309  ecopoprdm 5368  map0e 5401  map0 5403  mapsn 5404  en0 5482  en1 5485  fiprc 5492  pw2en 5505  ac6sfi 5509  sbthlem2 5511  sbthlem4 5513  sbthlem5 5514  fodomr 5547  mapxpen 5589  xpmapenlem5 5594  nneneq 5606  php3 5609  fodomfi 5656  supub 5670  suplub 5671  hartog 5693  sucprcreg 5703  inf3lemd 5718  inf3lem6 5724  noinfep 5747  trcl 5752  r1tr 5765  r1val1 5769  rankr1 5785  scottex 5846  scott0 5847  bnd2 5854  infenomsub 5889  ac6lem 5916  numth2 5947  cardval 5975  oncard 5978  cardidm 6001  cardlim 6003  ondomon 6008  cardprc 6013  cardaleph 6033  cfub 6056  cflecard 6060  cfle 6061  cfsuc 6063  axpowndlem3 6103  indpi 6186  distrpqlem 6218  1pr 6269  ltsopr 6288  prlem934b 6290  recexpr 6312  1ne0sr 6357  0idsr 6358  00sr 6360  recexsrlem 6364  leid 6701  mnfltxr 6720  xrlttri 6727  xrlttr 6728  xrleid 6735  lelttric 6805  lemul1a 7019  lemul1aOLD 7020  posexi 7091  nn1suc 7122  xrub 7289  nn0sub 7370  zltp1le 7390  nn0ind-raph 7426  elq 7437  qbtwnxr 7460  shftfn 7756  limsupcl 7773  seqzfn 7782  seqzres 7803  seqzres2 7804  expne0i 7830  0exp 7832  expwordi 7848  sqr0 7922  sqrlem6 7928  sqrmsqi 7959  sqr2irrlem1 7974  replim 8011  recvalzi 8139  abs1mi 8156  faclbnd4lem1 8200  mulc1cncf 8541  efcltlem1 8566  egt2OLD 8657  egt2lt3 8659  ruclem36 8814  infxpidmlem7 8827  infmap2 8850  eltg3 8896  islp2 9023  qdensere 9027  cnsscnp 9049  met0 9092  metn0 9098  blf 9121  lmrel 9205  subgrnss 9428  gapm 9462  ringsn 9490  nvmid 9617  ubthlem8 9879  efifolem6 10081  grothpw 10134  setwoe 10170  dif1enOLD 10173  indexfi 10174  findcard 10178  findcardOLD 10179  abfi2 10216  tx1cn 10223  tx2cn 10224  elsubsp 10248  stoig 10251  subcld 10254  subtopmetlem 10255  fbssint 10279  dirref 10355  ismgm 10367  unmnd 10405  on1el4 10413  zrdivrng 10418  hiidrcl 10594  hsn0elch 10753  ocsh 10789  hsupunss 10946  spanss2 10947  shjshseli 11049  cmbr4i 11177  dfiop2 11316  kbpj 11517  nmopun 11576  adjbdln 11653  adjeq0 11661  pjssdif1i 11747  pjinvari 11764  pjcmmul2i 11775  pj3i 11781  stge1i 11810  stle0i 11811  mdsymi 11983  sumdmdlem2 11991  dmdbr6ati 11995  dmdbr7ati 11996  bnj116 12460  bnj142 12474  bnj143 12475  bnj216 12507  bnj922 12834  bnj1143 12942  bnj151 13243  bnj218 13250  bnj1014 13374  bnj1145 13431  bnj1498 13562  elnn00nn 13602  suprzcl 13658  0dvds 13675  gcddvds 13722  gcdcl 13724  1nprm 13769  3prm 13780  fvrn0 13837  dfon2lem7 13855  dford4lem1 13859  trcllem1 13933  frxp 13951  wfrlem4 13960  wfrlem6 13962  wfrlem14 13970  wfrlem15 13971  nosgnn0i 14000  axfelem1 14031  axfelem3 14033  axfelem4 14034  axfelem5 14035  axfelem7 14037  axfelem8 14038  axfelem9 14039  brbigcup 14074  altopth1sn 14090  elaltxp 14098  stcat 14347  ump 14349  scprefat 14380  scprefat2 14381  imfstnrelc 14396  set2elt 14408  r1subsuc 14439  prmapcp3 14498  valcurfn1 14552  preoref22 14570  posprs 14581  defge3 14613  inposet 14620  dispos 14632  clfsebs2 14710  isppm 14715  svs2 14829  svs3 14830  oibbi1 14853  oibbi2 14854  hmeogrp 14892  top1 14896  top2ind 14897  subspemp 14903  rcfpfillem5 14932  rcfpfil 14934  limfilnei 14943  bwt2 14960  clindistop 14962  idtrgrp 14978  trhom 14983  tpgprop1 14986  cntrsetlem 14999  lteqtpos 15024  dualded 15132  catsbc 15197  empistar 15219  inacint 15221  tarsin 15230  elttar 15253  tmpts 15257  tartarmap 15265  elfiun 15369  hartogOLD 15384  infenomsubOLD 15398  subcls 15424  compsublem 15430  compsub 15431  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  alexsublem2 15438  alexsublem3 15439  alexsub 15441  connsub 15443  fneref 15493  refref 15494  neibastop2lem3 15521  neibastop2lem4 15522  topmeet 15526  topjoin 15527  fnejoin2 15531  filfinnfr 15561  ufileu 15573  fixufil 15576  filcon 15580  rnelfm 15593  fmfnfmlem2 15595  fcluscf 15612  flimfnfcls 15615  fcluscomp 15621  sfclusf 15624  upixp 15729  findcard2 15745  fimax 15746  indexfiOLD 15755  inficl 15757  fzfi2 15787  sdc 15811  cncfco 15887  piececn 15894  heiborlem6 15960  heiborlem13 15967  heiborlem18 15972  heiborlem21 15975  rrntotbnd 16022  grpkerinj 16042  phtpycolem2 16052  isphtpc2 16060  pcocn 16076  pcoloopf 16079  isdivrng1 16109  divrngcl 16110  isdivrng2 16111  igenss 16210  prtlem12 16270  emhgrat 16297  ipo0 16426  ifr0 16427  addrfn 16472  subrfn 16473  mulvfn 16474  eustrdif 16722  isline 17220  ispoint 17223  0psub 17230  linepsub 17232  atpsub 17233

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 164

Copyright terms: Public domain