Theorem mpbiri 168

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

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	. . 3 |- ch
2	1	a1i 9	. 2 |- ( ph -> ch )
3		mpbiri.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbird 167	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.18im  1430  ceqsexv2d  2856  dedhb  2989  sbceqal  3101  ssdifeq0  3596  pwidg  3691  elpr2  3716  snidg  3723  exsnrex  3736  rabrsndc  3764  prid1g  3800  tpid1g  3809  tpid2g  3811  sssnr  3862  ssprr  3865  sstpr  3866  preqr1  3877  unimax  3953  intmin3  3981  eqbrtrdi  4153  if0elpw  4276  pwnss  4277  0inp0  4284  bnd2  4291  ss1o0el1  4315  exmidsssn  4320  exmidundif  4324  exmidundifim  4325  euabex  4346  copsexg  4365  euotd  4376  elopab  4381  epelg  4416  sucidg  4542  ifelpwung  4607  regexmidlem1  4660  sucprcreg  4676  onprc  4679  dtruex  4686  omelon2  4735  elvvuni  4819  eqrelriv  4848  relopabi  4885  opabid2  4891  ididg  4913  iss  5089  funopg  5391  fn0  5483  f00  5564  f0bi  5565  f10d  5655  f1o00  5656  fo00  5657  brprcneu  5668  relelfvdm  5707  fvmbr  5710  fsn  5854  funop  5866  eufnfv  5922  f1eqcocnv  5970  riotaprop  6037  acexmidlemb  6050  acexmidlemab  6052  acexmidlem2  6055  oprabid  6090  elrnmpo  6175  ov6g  6200  eqop2  6385  1stconst  6430  2ndconst  6431  dftpos3  6506  dftpos4  6507  2pwuninelg  6527  frecabcl  6643  el2oss1o  6689  ecopover  6880  map0g  6935  mapsnd  6936  mapsn  6938  elixpsn  6983  en0  7048  en1  7052  fiprc  7070  en2m  7079  dom0  7104  nneneq  7124  findcard  7158  findcard2  7159  findcard2s  7160  elssdc  7175  eqsndc  7176  sbthlem2  7241  sbthlemi4  7243  sbthlemi5  7244  2omap  7282  eldju2ndl  7376  updjudhf  7383  enumct  7419  nnnninf  7430  nninfisollem0  7434  fodjuomnilemdc  7448  exmidonfinlem  7509  exmidaclem  7528  pw1ne1  7552  pw1ne3  7553  1ne0sr  8097  00sr  8100  cnm  8163  eqlei2  8384  cnstab  8937  divcanap3  8992  sup3exmid  9251  nn1suc  9276  nn0ge0  9541  xnn0xr  9588  xnn0nemnf  9594  elnn0z  9610  nn0n0n1ge2b  9678  nn0ind-raph  9716  elnn1uz2  9960  indstr2  9962  xrnemnf  10132  xrnepnf  10133  mnfltxr  10141  nn0pnfge0  10146  xrlttr  10150  xrltso  10151  xrlttri3  10152  nltpnft  10169  npnflt  10170  ngtmnft  10172  nmnfgt  10173  xsubge0  10236  xposdif  10237  xleaddadd  10242  fztpval  10442  fseq1p1m1  10453  fz01or  10470  qbtwnxr  10644  xqltnle  10654  fzfig  10819  uzsinds  10833  ser0f  10923  1exp  10957  0exp  10963  bcn1  11148  en1hash  11191  hashfibc  11235  zfz1iso  11241  hash2en  11243  0wrd0  11278  wrdlen1  11290  wrdl1exs1  11345  swrdspsleq  11387  cats1un  11441  wrdind  11442  wrd2ind  11443  sq01  11608  sqrt0rlem  11717  fzf1o  12090  prodf1f  12258  0dvds  12526  nn0o  12622  flodddiv4  12651  bitsp1o  12668  gcddvds  12688  bezoutlemmain  12723  lcmdvds  12805  rpdvds  12825  1nprm  12840  prmind2  12846  nnoddn2prmb  12989  pcpre1  13019  qexpz  13079  4sqlem19  13136  ballotfilem8  13228  ennnfonelemj0  13240  ennnfonelemhf1o  13252  strslfv  13345  restsspw  13550  xpsfrnel  13612  mgmidcl  13645  mgmlrid  13646  releqgg  13977  gsumgfsum1  14107  islidlm  14757  zrhrhm  14901  psrplusgg  14963  baspartn  15045  eltg3  15052  topnex  15081  discld  15131  cnpfval  15190  cnprcl2k  15201  idcn  15207  xmet0  15358  blfvalps  15380  blfps  15404  blf  15405  limcimolemlt  15659  recnprss  15682  lgsdir2lem2  16032  gausslemma2dlem4  16067  2lgslem2  16095  2lgslem3  16104  2lgs  16107  2sqlem7  16124  uhgr0e  16207  incistruhgr  16215  issubgr2  16383  subgrprop2  16385  egrsubgr  16388  0grsubgr  16389  0uhgrsubgr  16390  uhgrsubgrself  16391  clwwlkn1  16543  funmptd  16715  bj-om  16847  bj-nn0suc0  16860  bj-nn0suc  16874  bj-nn0sucALT  16888  bj-findis  16889  pw1map  16909  nninfall  16927  nnnninfen  16939  trilpolemcl  16961  dceqnconst  16985  dcapnconst  16986