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  4042  neldif  4074  reuss2  4266  pssdifn0  4308  dfiun2g  4972  elinxp  5984  ordunidif  6373  eceqoveq  8769  infxpenlem  9935  ackbij1lem18  10158  isf32lem2  10276  ingru  10738  indpi  10830  nqereu  10852  elpq  12925  elfz0ubfz0  13586  elfzmlbp  13593  elfzo0z  13656  fzofzim  13664  fzo1fzo0n0  13670  elfzodifsumelfzo  13686  swrdswrd  14667  swrdccatin1  14687  swrd2lsw  14914  p1modz1  16228  dfgcd2  16515  algcvga  16548  pcprendvds  16811  restntr  23147  filconn  23848  filssufilg  23876  ufileu  23884  ufilen  23895  alexsubALTlem3  24014  blcld  24470  causs  25265  itg2addlem  25725  rplogsum  27490  ltsres  27626  wlkonl1iedg  29732  trlf1  29765  spthdifv  29801  upgrwlkdvde  29805  usgr2pth  29832  pthdlem2  29836  uspgrn2crct  29876  crctcshwlkn0  29889  clwlkclwwlklem2  30070  clwwlknon0  30163  3spthd  30246  ofpreima2  32739  esumpinfval  34217  eulerpartlemf  34514  fin2so  37928  fdc  38066  lshpcmp  39434  lfl1  39516  frege124d  44188  onfrALTlem2  44973  3ornot23VD  45273  ordelordALTVD  45293  onfrALTlem2VD  45315  ndmaovass  47654  elfz2z  47763  lighneallem4  48073