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  7318  eldju2ndl  7412  updjudhf  7419  enumct  7455  nnnninf  7466  nninfisollem0  7470  fodjuomnilemdc  7484  exmidonfinlem  7545  exmidaclem  7564  pw1ne1  7588  pw1ne3  7589  1ne0sr  8133  00sr  8136  cnm  8199  eqlei2  8420  cnstab  8973  divcanap3  9028  sup3exmid  9287  nn1suc  9323  nn0ge0  9588  xnn0xr  9635  xnn0nemnf  9641  elnn0z  9657  nn0n0n1ge2b  9725  nn0ind-raph  9763  elnn1uz2  10007  indstr2  10009  xrnemnf  10179  xrnepnf  10180  mnfltxr  10188  nn0pnfge0  10193  xrlttr  10197  xrltso  10198  xrlttri3  10199  nltpnft  10216  npnflt  10217  ngtmnft  10219  nmnfgt  10220  xsubge0  10283  xposdif  10284  xleaddadd  10289  fztpval  10490  fseq1p1m1  10501  fz01or  10518  qbtwnxr  10692  xqltnle  10702  fzfig  10867  uzsinds  10881  ser0f  10971  1exp  11005  0exp  11011  bcn1  11196  en1hash  11239  hashfibc  11283  hashf1  11287  zfz1iso  11293  hash2en  11295  0wrd0  11330  wrdlen1  11342  wrdl1exs1  11397  swrdspsleq  11439  cats1un  11493  wrdind  11494  wrd2ind  11495  sq01  11660  sqrt0rlem  11769  fzf1o  12142  prodf1f  12310  0dvds  12578  nn0o  12674  flodddiv4  12703  bitsp1o  12720  gcddvds  12740  bezoutlemmain  12775  lcmdvds  12857  rpdvds  12877  1nprm  12892  prmind2  12898  nnoddn2prmb  13041  pcpre1  13071  qexpz  13131  4sqlem19  13188  ballotfilem8  13280  ennnfonelemj0  13292  ennnfonelemhf1o  13304  strslfv  13397  restsspw  13603  xpsfrnel  13665  mgmidcl  13698  mgmlrid  13699  releqgg  14023  gzsumgsum1  14153  islidlm  14816  zrhrhm  14958  psrplusgg  15069  baspartn  15151  eltg3  15158  topnex  15187  discld  15237  cnpfval  15296  cnprcl2k  15307  idcn  15313  xmet0  15464  blfvalps  15486  blfps  15510  blf  15511  limcimolemlt  15765  recnprss  15788  lgsdir2lem2  16152  gausslemma2dlem4  16187  2lgslem2  16215  2lgslem3  16224  2lgs  16227  2sqlem7  16244  uhgr0e  16327  incistruhgr  16335  issubgr2  16503  subgrprop2  16505  egrsubgr  16508  0grsubgr  16509  0uhgrsubgr  16510  uhgrsubgrself  16511  clwwlkn1  16663  funmptd  16835  bj-om  16967  bj-nn0suc0  16980  bj-nn0suc  16994  bj-nn0sucALT  17008  bj-findis  17009  pw1map  17029  wexmiddiffilem  17047  wexmiddifxylem  17049  nninfall  17056  nnnninfen  17068  trilpolemcl  17090  dceqnconst  17114  dcapnconst  17115