Theorem mpbiri 224

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  dedt  923  nfald2  1972  nfabd2  2507  dedhb  3006  sbceqal  3097  ssdifeq0  3632  r19.2zb  3640  dedth  3703  pwidg  3734  elpr2  3752  snidg  3758  ifpr  3774  prid1g  3825  pwpw0  3855  sssn  3864  pwsnALT  3882  unimax  3925  intmin3  3954  preqr1  4124  el1c  4139  eqpw1  4162  elxpk  4196  opkabssvvk  4208  cokrelk  4284  abexv  4324  eqpw1uni  4330  pw1equn  4331  pw1eqadj  4332  sspw12  4336  iotassuni  4355  0cnsuc  4401  nnc0suc  4412  nnsucelr  4428  nndisjeq  4429  snfi  4431  lefinrflx  4467  lenltfin  4469  ncfinprop  4474  ncfinraise  4481  ncfinlower  4483  tfinltfinlem1  4500  evenodddisj  4516  sfintfin  4532  sfinltfin  4535  vfinspsslem1  4550  vfinspss  4551  proj1op  4600  copsexg  4607  syl6eqbr  4676  elopab  4696  brsi  4761  br1st  4858  br2nd  4859  brswap2  4860  ididg  4871  iss  5000  dmxpss  5052  xpexr  5109  fn0  5202  f00  5249  f1o00  5317  fo00  5318  dffn5  5363  fvopab4t  5385  fsn  5432  fvi  5442  fconstfv  5456  brswap  5509  oprabid  5550  ov6g  5600  ovelrn  5608  caovmo  5645  op1st2nd  5790  txpcofun  5803  mapsspm  6021  mapsspw  6022  map0e  6023  map0  6025  mapsn  6026  en0  6042  xpassen  6057  enprmaplem5  6080  nenpw1pwlem2  6085  elncs  6119  ncseqnc  6128  eqnc2  6129  1cnc  6139  ncdisjeq  6148  peano4nc  6150  2p1e3c  6156  eqtc  6161  ce0addcnnul  6179  ce0nnulb  6182  ncpw1pwneg  6201  sbthlem1  6203  sbth  6206  addlec  6208  nc0le1  6216  leconnnc  6218  addceq0  6219  dflec3  6221  lenc  6223  tc11  6228  taddc  6229  letc  6231  ce0t  6232  ce2le  6233  ce0lenc1  6239  addcdi  6250  muc0or  6252  0lt1c  6258  spacid  6285  nchoicelem9  6297  nchoicelem14  6302  nchoicelem17  6305  nchoicelem19  6307  frecsuc  6322  scancan  6331