Theorem simplbi2 506

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 418	1 ⊢ (𝜓 → (𝜒 → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simplbi2com  508  sspss  4050  neldif  4081  reuss2  4272  pssdifn0  4316  dfiun2g  4988  elinxp  6010  ordunidif  6406  eceqoveq  8827  infxpenlem  10073  ackbij1lem18  10295  isf32lem2  10413  ingru  10881  indpi  10973  nqereu  10995  elpq  13084  elfz0ubfz0  13746  elfzmlbp  13753  elfzo0z  13816  fzofzim  13824  fzo1fzo0n0  13830  elfzodifsumelfzo  13846  swrdswrd  14834  swrdccatin1  14854  swrd2lsw  15085  p1modz1  16409  dfgcd2  16699  algcvga  16734  pcprendvds  16998  restntr  23480  filconn  24182  filssufilg  24210  ufileu  24218  ufilen  24229  alexsubALTlem3  24348  blcld  24804  causs  25599  itg2addlem  26059  rplogsum  27836  ltsres  28001  wlkonl1iedg  30226  trlf1  30263  spthdifv  30301  upgrwlkdvde  30305  usgr2pth  30332  pthdlem2  30336  uspgrn2crct  30379  crctcshwlkn0  30392  clwlkclwwlklem2  30573  clwwlknon0  30666  3spthd  30759  ofpreima2  33242  esumpinfval  34687  eulerpartlemf  34985  fin2so  38498  fdc  38647  lshpcmp  40013  lfl1  40095  frege124d  44720  onfrALTlem2  45488  3ornot23VD  45788  ordelordALTVD  45808  onfrALTlem2VD  45830  ndmaovass  48220  elfz2z  48329  lighneallem4  48639