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  4058  neldif  4090  reuss2  4281  pssdifn0  4324  dfiun2g  4990  elinxp  6009  ordunidif  6400  eceqoveq  8808  infxpenlem  9985  ackbij1lem18  10207  isf32lem2  10326  ingru  10788  indpi  10880  nqereu  10902  elpq  12990  elfz0ubfz0  13651  elfzmlbp  13658  elfzo0z  13721  fzofzim  13729  fzo1fzo0n0  13735  elfzodifsumelfzo  13751  swrdswrd  14732  swrdccatin1  14752  swrd2lsw  14979  p1modz1  16307  dfgcd2  16594  algcvga  16627  pcprendvds  16890  restntr  23300  filconn  24001  filssufilg  24029  ufileu  24037  ufilen  24048  alexsubALTlem3  24167  blcld  24623  causs  25418  itg2addlem  25878  rplogsum  27649  ltsres  27784  wlkonl1iedg  29922  trlf1  29955  spthdifv  29991  upgrwlkdvde  29995  usgr2pth  30022  pthdlem2  30026  uspgrn2crct  30066  crctcshwlkn0  30079  clwlkclwwlklem2  30260  clwwlknon0  30353  3spthd  30436  ofpreima2  32923  esumpinfval  34380  eulerpartlemf  34677  fin2so  38118  fdc  38256  lshpcmp  39624  lfl1  39706  frege124d  44349  onfrALTlem2  45120  3ornot23VD  45420  ordelordALTVD  45440  onfrALTlem2VD  45462  ndmaovass  47798  elfz2z  47907  lighneallem4  48217