Theorem pm2.61ian 824

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
pm2.61ian.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.61ian.2	⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
pm2.61ian	⊢ (𝜓 → 𝜒)

Proof of Theorem pm2.61ian

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 418	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 184	1 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ 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:  4cases  1056  cases2ALT  1064  consensus  1068  preqsnd  4819  csbexg  5264  snopeqop  5478  xpcan2  6169  tfindsg  7870  findsg  7907  ixpexg  8943  fipwss  9414  ranklim  9851  fin23lem14  10404  fzoval  13787  modsumfzodifsn  14080  hashge2el2dif  14618  iswrdi  14655  swrd0  14801  swrdsbslen  14807  swrdspsleq  14808  pfxccatin12  14875  swrdccat  14877  pfxccat3a  14880  repswswrd  14928  cshword  14935  cshwcsh2id  14972  dvdsabseq  16476  m1exp1  16539  flodddiv4  16578  dfgcd2  16712  lcmftp  16804  prmop1  17209  fvprmselelfz  17215  ressbas  17407  resseqnbas  17413  ressinbas  17416  cntzval  19528  symg2bas  19600  sralem  21444  srasca  21448  sravsca  21449  sraip  21450  isfieldidl  21533  ocvval  21966  dsmmval  22033  dmatmul  22805  1mavmul  22856  mavmul0g  22861  1marepvmarrepid  22883  smadiadetglem2  22980  1elcpmat  23026  decpmatid  23081  tnglem  24952  tngds  24960  gausslemma2dlem1a  27685  2lgslem1c  27713  2sqreulem1  27766  2sqreunnlem1  27769  nosupno  28053  nosupbday  28055  nosupbnd1lem5  28062  nosupbnd1  28064  nosupbnd2  28066  noinfno  28068  noinfbday  28070  noinfbnd1lem5  28077  noinfbnd1  28079  noinfbnd2  28081  madess  28245  abssge0  28624  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwwisshclwwsn  30600  clwwlknon1nloop  30683  eucrctshift  30837  eucrct2eupth  30839  unopbd  32610  nmopcoi  32690  resvsca  33886  resvlem  33887  satfv1lem  36106  bj-prmoore  38016  ax12indalem  39982  afvres  48211  afvco2  48215  2ffzoeq  48367  difmodm1lt  48404  ply1mulgsumlem2  49468  lcoel0  49509  lindslinindsimp1  49538  digexp  49688  dig1  49689  itsclc0yqsol  49845