Theorem simplbi2 505

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
simplbi2.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi2	⊢ (𝜓 → (𝜒 → 𝜑))

Proof of Theorem simplbi2

Step	Hyp	Ref	Expression
1		simplbi2.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpri 231	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 417	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simplbi2com  507  sspss  4057  neldif  4089  reuss2  4280  pssdifn0  4324  dfiun2g  4995  elinxp  6020  ordunidif  6413  eceqoveq  8821  infxpenlem  9998  ackbij1lem18  10220  isf32lem2  10339  ingru  10801  indpi  10893  nqereu  10915  elpq  13000  elfz0ubfz0  13662  elfzmlbp  13669  elfzo0z  13732  fzofzim  13740  fzo1fzo0n0  13746  elfzodifsumelfzo  13762  swrdswrd  14744  swrdccatin1  14764  swrd2lsw  14991  p1modz1  16318  dfgcd2  16605  algcvga  16638  pcprendvds  16901  restntr  23320  filconn  24021  filssufilg  24049  ufileu  24057  ufilen  24068  alexsubALTlem3  24187  blcld  24643  causs  25438  itg2addlem  25898  rplogsum  27669  ltsres  27804  wlkonl1iedg  29991  trlf1  30024  spthdifv  30060  upgrwlkdvde  30064  usgr2pth  30091  pthdlem2  30095  uspgrn2crct  30135  crctcshwlkn0  30148  clwlkclwwlklem2  30329  clwwlknon0  30422  3spthd  30505  ofpreima2  32989  esumpinfval  34441  eulerpartlemf  34738  fin2so  38236  fdc  38374  lshpcmp  39740  lfl1  39822  frege124d  44467  onfrALTlem2  45235  3ornot23VD  45535  ordelordALTVD  45555  onfrALTlem2VD  45577  ndmaovass  47920  elfz2z  48029  lighneallem4  48339