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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.18im  1434  ceqsexv2d  2862  dedhb  2995  sbceqal  3107  ssdifeq0  3610  pwidg  3706  elpr2  3731  snidg  3738  exsnrex  3751  rabrsndc  3779  prid1g  3815  tpid1g  3825  tpid2g  3827  sssnr  3878  ssprr  3881  sstpr  3882  preqr1  3893  unimax  3969  intmin3  3997  eqbrtrdi  4169  if0elpw  4295  pwnss  4296  0inp0  4303  bnd2  4310  ss1o0el1  4334  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  euabex  4365  copsexg  4384  euotd  4395  elopab  4400  epelg  4435  sucidg  4561  ifelpwung  4627  regexmidlem1  4680  sucprcreg  4696  onprc  4699  dtruex  4706  omelon2  4755  elvvuni  4839  eqrelriv  4868  relopabi  4905  opabid2  4911  ididg  4933  iss  5109  funopg  5411  fn0  5503  f00  5584  f0bi  5585  f10d  5675  f1o00  5676  fo00  5677  brprcneu  5688  relelfvdm  5727  fvmbr  5731  fsn  5880  funop  5892  eufnfv  5949  f1eqcocnv  5997  riotaprop  6064  acexmidlemb  6077  acexmidlemab  6079  acexmidlem2  6082  oprabid  6117  elrnmpo  6202  ov6g  6227  eqop2  6412  1stconst  6457  2ndconst  6458  dftpos3  6533  dftpos4  6534  2pwuninelg  6554  frecabcl  6670  el2oss1o  6716  ecopover  6907  map0g  6969  mapsnd  6970  mapsn  6972  elixpsn  7017  en0  7082  en1  7086  fiprc  7104  en2m  7113  dom0  7138  nneneq  7158  findcard  7192  findcard2  7193  findcard2s  7194  elssdc  7209  eqsndc  7210  sbthlem2  7275  sbthlemi4  7277  sbthlemi5  7278  2omap  7319  eldju2ndl  7413  updjudhf  7420  enumct  7456  nnnninf  7467  nninfisollem0  7471  fodjuomnilemdc  7485  exmidonfinlem  7546  exmidaclem  7565  pw1ne1  7589  pw1ne3  7590  1ne0sr  8134  00sr  8137  cnm  8200  eqlei2  8422  cnstab  8976  divcanap3  9031  sup3exmid  9290  nn1suc  9326  nn0ge0  9593  xnn0xr  9640  xnn0nemnf  9646  elnn0z  9662  nn0n0n1ge2b  9730  nn0ind-raph  9768  elnn1uz2  10017  indstr2  10019  xrnemnf  10190  xrnepnf  10191  mnfltxr  10199  nn0pnfge0  10204  xrlttr  10208  xrltso  10209  xrlttri3  10210  nltpnft  10227  npnflt  10228  ngtmnft  10230  nmnfgt  10231  xsubge0  10294  xposdif  10295  xleaddadd  10300  fztpval  10501  fseq1p1m1  10512  fz01or  10529  qbtwnxr  10703  xqltnle  10713  fzfig  10881  uzsinds  10895  ser0f  10985  1exp  11019  0exp  11025  bcn1  11211  en1hash  11254  hashfibc  11298  hashf1  11302  zfz1iso  11308  hash2en  11310  0wrd0  11345  wrdlen1  11357  wrdl1exs1  11412  swrdspsleq  11454  cats1un  11508  wrdind  11509  wrd2ind  11510  sq01  11675  sqrt0rlem  11784  fzf1o  12160  prodf1f  12328  0dvds  12596  nn0o  12692  flodddiv4  12721  bitsp1o  12738  gcddvds  12758  bezoutlemmain  12793  lcmdvds  12875  rpdvds  12895  1nprm  12910  prmind2  12916  nnoddn2prmb  13063  pcpre1  13093  qexpz  13153  4sqlem19  13210  prmlem0  13242  ballotfilem8  13331  ennnfonelemj0  13343  ennnfonelemhf1o  13355  strslfv  13448  restsspw  13654  xpsfrnel  13716  mgmidcl  13749  mgmlrid  13750  releqgg  14074  gzsumgsum1  14204  islidlm  14867  zrhrhm  15009  psrplusgg  15121  baspartn  15203  eltg3  15210  topnex  15239  discld  15289  cnpfval  15348  cnprcl2k  15359  idcn  15365  xmet0  15516  blfvalps  15538  blfps  15562  blf  15563  limcimolemlt  15817  recnprss  15840  lgsdir2lem2  16270  gausslemma2dlem4  16305  2lgslem2  16333  2lgslem3  16342  2lgs  16345  2sqlem7  16362  uhgr0e  16445  incistruhgr  16453  issubgr2  16621  subgrprop2  16623  egrsubgr  16626  0grsubgr  16627  0uhgrsubgr  16628  uhgrsubgrself  16629  clwwlkn1  16781  funmptd  16953  bj-om  17085  bj-nn0suc0  17098  bj-nn0suc  17112  bj-nn0sucALT  17126  bj-findis  17127  pw1map  17147  wexmiddiffilem  17165  wexmiddifxylem  17167  nninfall  17174  nnnninfen  17186  trilpolemcl  17208  dceqnconst  17232  dcapnconst  17233