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	⊢ 𝜒
mpbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbiri	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 167	1 ⊢ (𝜑 → 𝜓)

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  ceqsexv2d  2803  dedhb  2933  sbceqal  3045  ssdifeq0  3534  pwidg  3620  elpr2  3645  snidg  3652  exsnrex  3665  rabrsndc  3691  prid1g  3727  tpid1g  3735  tpid2g  3737  sssnr  3784  ssprr  3787  sstpr  3788  preqr1  3799  unimax  3874  intmin3  3902  eqbrtrdi  4073  pwnss  4193  0inp0  4200  bnd2  4207  ss1o0el1  4231  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  euabex  4259  copsexg  4278  euotd  4288  elopab  4293  epelg  4326  sucidg  4452  ifelpwung  4517  regexmidlem1  4570  sucprcreg  4586  onprc  4589  dtruex  4596  omelon2  4645  elvvuni  4728  eqrelriv  4757  relopabi  4792  opabid2  4798  ididg  4820  iss  4993  funopg  5293  fn0  5380  f00  5452  f0bi  5453  f1o00  5542  fo00  5543  brprcneu  5554  relelfvdm  5593  fsn  5737  eufnfv  5796  f1eqcocnv  5841  riotaprop  5904  acexmidlemb  5917  acexmidlemab  5919  acexmidlem2  5922  oprabid  5957  elrnmpo  6040  ov6g  6065  eqop2  6245  1stconst  6288  2ndconst  6289  dftpos3  6329  dftpos4  6330  2pwuninelg  6350  frecabcl  6466  el2oss1o  6510  ecopover  6701  map0g  6756  mapsn  6758  elixpsn  6803  en0  6863  en1  6867  fiprc  6883  dom0  6908  nneneq  6927  findcard  6958  findcard2  6959  findcard2s  6960  sbthlem2  7033  sbthlemi4  7035  sbthlemi5  7036  eldju2ndl  7147  updjudhf  7154  enumct  7190  nnnninf  7201  nninfisollem0  7205  fodjuomnilemdc  7219  exmidonfinlem  7274  exmidaclem  7293  pw1ne1  7314  pw1ne3  7315  1ne0sr  7852  00sr  7855  cnm  7918  eqlei2  8140  cnstab  8691  divcanap3  8744  sup3exmid  9003  nn1suc  9028  nn0ge0  9293  xnn0xr  9336  xnn0nemnf  9342  elnn0z  9358  nn0n0n1ge2b  9424  nn0ind-raph  9462  elnn1uz2  9700  indstr2  9702  xrnemnf  9871  xrnepnf  9872  mnfltxr  9880  nn0pnfge0  9885  xrlttr  9889  xrltso  9890  xrlttri3  9891  nltpnft  9908  npnflt  9909  ngtmnft  9911  nmnfgt  9912  xsubge0  9975  xposdif  9976  xleaddadd  9981  fztpval  10177  fseq1p1m1  10188  fz01or  10205  qbtwnxr  10366  xqltnle  10376  fzfig  10541  uzsinds  10555  ser0f  10645  1exp  10679  0exp  10685  bcn1  10869  zfz1iso  10952  0wrd0  10980  wrdlen1  10991  sqrt0rlem  11187  prodf1f  11727  0dvds  11995  nn0o  12091  flodddiv4  12120  bitsp1o  12137  gcddvds  12157  bezoutlemmain  12192  lcmdvds  12274  rpdvds  12294  1nprm  12309  prmind2  12315  nnoddn2prmb  12458  pcpre1  12488  qexpz  12548  4sqlem19  12605  ennnfonelemj0  12645  ennnfonelemhf1o  12657  strslfv  12750  restsspw  12953  xpsfrnel  13048  mgmidcl  13082  mgmlrid  13083  releqgg  13428  islidlm  14113  zrhrhm  14257  psrplusgg  14308  baspartn  14372  eltg3  14379  topnex  14408  discld  14458  lmreltop  14515  cnpfval  14517  cnprcl2k  14528  idcn  14534  xmet0  14685  blfvalps  14707  blfps  14731  blf  14732  limcimolemlt  14986  recnprss  15009  lgsdir2lem2  15356  gausslemma2dlem4  15391  2lgslem2  15419  2lgslem3  15428  2lgs  15431  2sqlem7  15448  funmptd  15535  bj-om  15669  bj-nn0suc0  15682  bj-nn0suc  15696  bj-nn0sucALT  15710  bj-findis  15711  2omap  15728  nninfall  15742  nnnninfen  15754  trilpolemcl  15772  dceqnconst  15795  dcapnconst  15796