Theorem mpbiri 169

Description: An inference from a nested biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbiri.min	⊢ χ
mpbiri.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mpbiri	⊢ (φ → ψ)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. 2 ⊢ χ
2		mpbiri.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimprd 136	. 2 ⊢ (φ → (χ → ψ))
4	1, 3	mpi 44	1 ⊢ (φ → ψ)

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  dedt 572  rgen2 1248  class2set 1747  dedth 1784  dedth2v 1785  dedth3v 1786  elpw2g 1803  snidg 1828  sssn 1852  snsspr 1853  snex 1859  moabex 1868  preqr1 1872  pwpw0 1883  prex 1892  opth 1898  copsexg 1902  opprc1b 1906  opprc3 1908  euuni 1954  reucl 1957  reuuni3 1958  syl6eqbr 2092  elopab 2110  supub 2160  suplub 2161  onprc 2240  ordeleqon 2241  onint0 2262  ord0eln0 2278  nsuceq0 2306  ordunisuc 2339  0elsuc 2340  onuninsuc 2356  onun 2358  limsuc 2361  nlimsuc 2363  unizlim 2364  orduninsuc 2365  ordzsl 2366  onzsl 2367  limomss 2378  limom 2387  peano5 2394  tfinds 2401  opelxpex 2445  0nelxp 2475  relsn 2485  iss 2599  dfrel2 2660  coi1 2665  fn0 2739  zfrep6 2744  f00 2773  fconst 2774  f1o00 2823  fnopabfv 2858  fsn 2895  fvi 2900  fconst2 2902  fconstfv 2903  canth 2945  tfrlem6 2954  oprabval3 3052  ndmoprcl 3058  caoprmo 3084  oesuc 3134  omcl 3139  oecl 3140  oawordeulem 3156  oen0 3165  nnmcl 3173  ecopoprdm 3245  map0e 3266  mapsn 3269  en0 3328  en1 3331  xpsnen 3339  pw2en 3348  sbthlem2 3350  sbthlem4 3352  sbthlem5 3353  mapxpen 3390  xpmapenlem5 3395  nneneq 3408  php3 3411  sucprcreg 3451  inf0 3457  inf3lemd 3463  inf3lem6 3469  trcl 3489  r1tr 3498  r1ord 3499  r1val1 3502  rankon 3515  rankr1 3518  scottex 3541  scott0 3542  bnd2 3549  ac6lem 3575  numth2 3600  fodomb 3615  cardval 3633  oncard 3636  cardcard 3655  cardlim 3657  ondomon 3662  cardprc 3667  alephon 3671  alephcard 3673  alephordlem1 3677  cardaleph 3690  cardalephex 3691  cfub 3703  cardcf 3706  cflecard 3707  cfle 3708  cfsuc 3709  axpowndlem3 3745  indpi 3828  distrpqlem 3860  recclpq 3866  1pr 3911  ltsopr 3930  prlem934b 3932  recexpr 3954  1ne0sr 3999  0idsr 4000  00sr 4002  recexsrlem 4006  leidt 4293  eqneg 4378  posex 4422  nn1suc 4435  nn0subt 4587  znegclt 4588  elnn0nn 4593  zltp1let 4597  nn0ind 4612  elq 4629  sqr0 4730  sqrlem6 4736  sqrsqid 4766  sqr2irrlem1 4777  replimt 4798  reim0 4809  ruclem36 4920  ruclem37 4921  infxpidmlem7 4939  infmap2 4953  hsn0elch 5155  ocsh 5164  omlsilem 5249  pjoc1 5268  hsupunss 5314  spanss2 5315  shjshsel 5413  cmbr4 5510  pjssge0 5573  ho1 5613  pj3 5660  stge1 5679  stle0 5680  mdsym 5784  sumdmd 5787

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

This theorem depends on definitions:  df-bi 128

metamath.org