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  4813  csbexg  5263  snopeqop  5477  xpcan2  6168  tfindsg  7873  findsg  7910  ixpexg  8954  fipwss  9425  ranklim  9862  fin23lem14  10415  fzoval  13798  modsumfzodifsn  14091  hashge2el2dif  14629  iswrdi  14666  swrd0  14813  swrdsbslen  14819  swrdspsleq  14820  pfxccatin12  14887  swrdccat  14889  pfxccat3a  14892  repswswrd  14940  cshword  14947  cshwcsh2id  14984  dvdsabseq  16489  m1exp1  16552  flodddiv4  16591  dfgcd2  16725  lcmftp  16817  prmop1  17222  fvprmselelfz  17228  ressbas  17420  resseqnbas  17426  ressinbas  17429  cntzval  19541  symg2bas  19613  sralem  21457  srasca  21461  sravsca  21462  sraip  21463  isfieldidl  21546  ocvval  21979  dsmmval  22046  dmatmul  22818  1mavmul  22869  mavmul0g  22874  1marepvmarrepid  22896  smadiadetglem2  22993  1elcpmat  23039  decpmatid  23094  tnglem  24965  tngds  24973  gausslemma2dlem1a  27698  2lgslem1c  27726  2sqreulem1  27779  2sqreunnlem1  27782  nosupno  28066  nosupbday  28068  nosupbnd1lem5  28075  nosupbnd1  28077  nosupbnd2  28079  noinfno  28081  noinfbday  28083  noinfbnd1lem5  28090  noinfbnd1  28092  noinfbnd2  28094  madess  28258  abssge0  28637  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwwisshclwwsn  30613  clwwlknon1nloop  30696  eucrctshift  30850  eucrct2eupth  30852  unopbd  32623  nmopcoi  32703  resvsca  33940  resvlem  33941  acwer1prclem  35816  satfv1lem  36214  bj-prmoore  38129  ax12indalem  40096  afvres  48336  afvco2  48340  2ffzoeq  48492  difmodm1lt  48529  ply1mulgsumlem2  49593  lcoel0  49634  lindslinindsimp1  49663  digexp  49813  dig1  49814  itsclc0yqsol  49970