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  8936  divcanap3  8989  sup3exmid  9248  nn1suc  9273  nn0ge0  9538  xnn0xr  9585  xnn0nemnf  9591  elnn0z  9607  nn0n0n1ge2b  9675  nn0ind-raph  9713  elnn1uz2  9957  indstr2  9959  xrnemnf  10129  xrnepnf  10130  mnfltxr  10138  nn0pnfge0  10143  xrlttr  10147  xrltso  10148  xrlttri3  10149  nltpnft  10166  npnflt  10167  ngtmnft  10169  nmnfgt  10170  xsubge0  10233  xposdif  10234  xleaddadd  10239  fztpval  10439  fseq1p1m1  10450  fz01or  10467  qbtwnxr  10641  xqltnle  10651  fzfig  10816  uzsinds  10830  ser0f  10920  1exp  10954  0exp  10960  bcn1  11145  en1hash  11188  hashfibc  11232  zfz1iso  11238  hash2en  11240  0wrd0  11275  wrdlen1  11287  wrdl1exs1  11342  swrdspsleq  11384  cats1un  11438  wrdind  11439  wrd2ind  11440  sqrt0rlem  11713  fzf1o  12086  prodf1f  12254  0dvds  12522  nn0o  12618  flodddiv4  12647  bitsp1o  12664  gcddvds  12684  bezoutlemmain  12719  lcmdvds  12801  rpdvds  12821  1nprm  12836  prmind2  12842  nnoddn2prmb  12985  pcpre1  13015  qexpz  13075  4sqlem19  13132  ballotfilem8  13224  ennnfonelemj0  13236  ennnfonelemhf1o  13248  strslfv  13341  restsspw  13546  xpsfrnel  13641  mgmidcl  13675  mgmlrid  13676  releqgg  14021  islidlm  14739  zrhrhm  14883  psrplusgg  14945  baspartn  15027  eltg3  15034  topnex  15063  discld  15113  cnpfval  15172  cnprcl2k  15183  idcn  15189  xmet0  15340  blfvalps  15362  blfps  15386  blf  15387  limcimolemlt  15641  recnprss  15664  lgsdir2lem2  16014  gausslemma2dlem4  16049  2lgslem2  16077  2lgslem3  16086  2lgs  16089  2sqlem7  16106  uhgr0e  16189  incistruhgr  16197  issubgr2  16365  subgrprop2  16367  egrsubgr  16370  0grsubgr  16371  0uhgrsubgr  16372  uhgrsubgrself  16373  clwwlkn1  16525  funmptd  16687  bj-om  16819  bj-nn0suc0  16832  bj-nn0suc  16846  bj-nn0sucALT  16860  bj-findis  16861  pw1map  16881  nninfall  16899  nnnninfen  16911  trilpolemcl  16933  dceqnconst  16958  dcapnconst  16959  gsumgfsum1  16975