Theorem simplbi2 500

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 228	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 412	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simplbi2com  502  sspss  4054  neldif  4086  reuss2  4278  pssdifn0  4320  dfiun2g  4985  elinxp  5978  ordunidif  6367  eceqoveq  8759  infxpenlem  9923  ackbij1lem18  10146  isf32lem2  10264  ingru  10726  indpi  10818  nqereu  10840  elpq  12888  elfz0ubfz0  13548  elfzmlbp  13555  elfzo0z  13617  fzofzim  13625  fzo1fzo0n0  13631  elfzodifsumelfzo  13647  swrdswrd  14628  swrdccatin1  14648  swrd2lsw  14875  p1modz1  16186  dfgcd2  16473  algcvga  16506  pcprendvds  16768  restntr  23126  filconn  23827  filssufilg  23855  ufileu  23863  ufilen  23874  alexsubALTlem3  23993  blcld  24449  causs  25254  itg2addlem  25715  rplogsum  27494  ltsres  27630  wlkonl1iedg  29737  trlf1  29770  spthdifv  29806  upgrwlkdvde  29810  usgr2pth  29837  pthdlem2  29841  uspgrn2crct  29881  crctcshwlkn0  29894  clwlkclwwlklem2  30075  clwwlknon0  30168  3spthd  30251  ofpreima2  32744  esumpinfval  34230  eulerpartlemf  34527  fin2so  37804  fdc  37942  lshpcmp  39244  lfl1  39326  frege124d  43998  onfrALTlem2  44783  3ornot23VD  45083  ordelordALTVD  45103  onfrALTlem2VD  45125  ndmaovass  47448  elfz2z  47557  lighneallem4  47852