Theorem mpbir2an 948

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbir2an.1	⊢ 𝜓
mpbir2an.2	⊢ 𝜒
mpbiran2an.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbir2an	⊢ 𝜑

Proof of Theorem mpbir2an

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 ⊢ 𝜒
2		mpbir2an.1	. . 3 ⊢ 𝜓
3		mpbiran2an.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4	2, 3	mpbiran 946	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 146	1 ⊢ 𝜑

Syntax hints:   ∧ wa 104   ↔ 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:  3pm3.2i  1199  euequ1  2173  eqssi  3240  elini  3388  dtruarb  4275  opnzi  4321  so0  4417  we0  4452  ord0  4482  ordon  4578  onsucelsucexmidlem1  4620  regexmidlemm  4624  ordpwsucexmid  4662  reg3exmidlemwe  4671  ordom  4699  funi  5350  funcnvsn  5366  funinsn  5370  fnresi  5441  fn0  5443  f0  5518  fconst  5523  f10  5608  f1o0  5612  f1oi  5613  f1osn  5615  funopsn  5819  isoid  5940  iso0  5947  acexmidlem2  6004  fo1st  6309  fo2nd  6310  iordsmo  6449  tfrlem7  6469  tfrexlem  6486  mapsnf1o2  6851  1domsn  6984  inresflem  7235  0ct  7282  infnninf  7299  infnninfOLD  7300  exmidonfinlem  7379  exmidaclem  7398  pw1on  7419  sucpw1nel3  7426  1pi  7510  prarloclemcalc  7697  ltsopr  7791  ltsosr  7959  cnm  8027  axicn  8058  axaddf  8063  axmulf  8064  nnindnn  8088  mpomulf  8144  ltso  8232  negiso  9110  nnind  9134  0z  9465  dfuzi  9565  cnref1o  9854  elrpii  9860  xrltso  10000  0e0icopnf  10183  0e0iccpnf  10184  fz0to4untppr  10328  fldiv4p1lem1div2  10533  expcl2lemap  10781  expclzaplem  10793  expge0  10805  expge1  10806  xrnegiso  11781  fclim  11813  eff2  12199  reeff1  12219  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  egt2lt3  12299  halfleoddlt  12413  2prm  12657  3prm  12658  1arith  12898  setsslnid  13092  xpsff1o  13390  isabli  13845  rngmgpf  13908  mgpf  13982  zringnzr  14574  fntopon  14706  istpsi  14721  ismeti  15028  cnfldms  15218  tgqioo  15237  addcncntoplem  15243  divcnap  15247  abscncf  15267  recncf  15268  imcncf  15269  cjcncf  15270  maxcncf  15297  mincncf  15298  dveflem  15408  reeff1o  15455  reefiso  15459  ioocosf1o  15536  lgslem2  15688  lgsfcl2  15693  lgsne0  15725  2lgslem1b  15776  umgrbien  15918  ex-fl  16113  bj-indint  16318  bj-omord  16347  012of  16386  2o01f  16387  0nninf  16400  peano4nninf  16402  taupi  16471