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  1396  dedhb  2929  sbceqal  3041  ssdifeq0  3529  pwidg  3615  elpr2  3640  snidg  3647  exsnrex  3660  rabrsndc  3686  prid1g  3722  tpid1g  3730  tpid2g  3732  sssnr  3779  ssprr  3782  sstpr  3783  preqr1  3794  unimax  3869  intmin3  3897  eqbrtrdi  4068  pwnss  4188  0inp0  4195  bnd2  4202  ss1o0el1  4226  exmidsssn  4231  exmidundif  4235  exmidundifim  4236  euabex  4254  copsexg  4273  euotd  4283  elopab  4288  epelg  4321  sucidg  4447  ifelpwung  4512  regexmidlem1  4565  sucprcreg  4581  onprc  4584  dtruex  4591  omelon2  4640  elvvuni  4723  eqrelriv  4752  relopabi  4787  opabid2  4793  ididg  4815  iss  4988  funopg  5288  fn0  5373  f00  5445  f0bi  5446  f1o00  5535  fo00  5536  brprcneu  5547  relelfvdm  5586  fsn  5730  eufnfv  5789  f1eqcocnv  5834  riotaprop  5897  acexmidlemb  5910  acexmidlemab  5912  acexmidlem2  5915  oprabid  5950  elrnmpo  6032  ov6g  6056  eqop2  6231  1stconst  6274  2ndconst  6275  dftpos3  6315  dftpos4  6316  2pwuninelg  6336  frecabcl  6452  el2oss1o  6496  ecopover  6687  map0g  6742  mapsn  6744  elixpsn  6789  en0  6849  en1  6853  fiprc  6869  dom0  6894  nneneq  6913  findcard  6944  findcard2  6945  findcard2s  6946  sbthlem2  7017  sbthlemi4  7019  sbthlemi5  7020  eldju2ndl  7131  updjudhf  7138  enumct  7174  nnnninf  7185  nninfisollem0  7189  fodjuomnilemdc  7203  exmidonfinlem  7253  exmidaclem  7268  pw1ne1  7289  pw1ne3  7290  1ne0sr  7826  00sr  7829  cnm  7892  eqlei2  8114  cnstab  8664  divcanap3  8717  sup3exmid  8976  nn1suc  9001  nn0ge0  9265  xnn0xr  9308  xnn0nemnf  9314  elnn0z  9330  nn0n0n1ge2b  9396  nn0ind-raph  9434  elnn1uz2  9672  indstr2  9674  xrnemnf  9843  xrnepnf  9844  mnfltxr  9852  nn0pnfge0  9857  xrlttr  9861  xrltso  9862  xrlttri3  9863  nltpnft  9880  npnflt  9881  ngtmnft  9883  nmnfgt  9884  xsubge0  9947  xposdif  9948  xleaddadd  9953  fztpval  10149  fseq1p1m1  10160  fz01or  10177  qbtwnxr  10326  xqltnle  10336  fzfig  10501  uzsinds  10515  ser0f  10605  1exp  10639  0exp  10645  bcn1  10829  zfz1iso  10912  0wrd0  10940  wrdlen1  10951  sqrt0rlem  11147  prodf1f  11686  0dvds  11954  nn0o  12048  flodddiv4  12075  gcddvds  12100  bezoutlemmain  12135  lcmdvds  12217  rpdvds  12237  1nprm  12252  prmind2  12258  nnoddn2prmb  12400  pcpre1  12430  qexpz  12490  4sqlem19  12547  ennnfonelemj0  12558  ennnfonelemhf1o  12570  strslfv  12663  restsspw  12860  xpsfrnel  12927  mgmidcl  12961  mgmlrid  12962  releqgg  13290  islidlm  13975  zrhrhm  14111  psrplusgg  14162  baspartn  14218  eltg3  14225  topnex  14254  discld  14304  lmreltop  14361  cnpfval  14363  cnprcl2k  14374  idcn  14380  xmet0  14531  blfvalps  14553  blfps  14577  blf  14578  limcimolemlt  14818  recnprss  14841  lgsdir2lem2  15145  gausslemma2dlem4  15180  2sqlem7  15208  funmptd  15295  bj-om  15429  bj-nn0suc0  15442  bj-nn0suc  15456  bj-nn0sucALT  15470  bj-findis  15471  nninfall  15499  nnnninfen  15511  trilpolemcl  15527  dceqnconst  15550  dcapnconst  15551