Theorem pm2.61ian 811

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 412	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 182	1 ⊢ (𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ 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:  4cases  1040  cases2ALT  1048  consensus  1052  preqsnd  4826  csbexg  5268  snopeqop  5469  xpcan2  6153  tfindsg  7840  findsg  7876  ixpexg  8898  fipwss  9387  ranklim  9804  fin23lem14  10293  fzoval  13628  modsumfzodifsn  13916  hashge2el2dif  14452  iswrdi  14489  swrd0  14630  swrdsbslen  14636  swrdspsleq  14637  pfxccatin12  14705  swrdccat  14707  pfxccat3a  14710  repswswrd  14756  cshword  14763  cshwcsh2id  14801  dvdsabseq  16290  m1exp1  16353  flodddiv4  16392  dfgcd2  16523  lcmftp  16613  prmop1  17016  fvprmselelfz  17022  ressbas  17213  resseqnbas  17219  ressinbas  17222  cntzval  19260  symg2bas  19330  sralem  21090  srasca  21094  sravsca  21095  sraip  21096  ocvval  21583  dsmmval  21650  dmatmul  22391  1mavmul  22442  mavmul0g  22447  1marepvmarrepid  22469  smadiadetglem2  22566  1elcpmat  22609  decpmatid  22664  tnglem  24535  tngds  24543  gausslemma2dlem1a  27283  2lgslem1c  27311  2sqreulem1  27364  2sqreunnlem1  27367  nosupno  27622  nosupbday  27624  nosupbnd1lem5  27631  nosupbnd1  27633  nosupbnd2  27635  noinfno  27637  noinfbday  27639  noinfbnd1lem5  27646  noinfbnd1  27648  noinfbnd2  27650  madess  27795  abssge0  28154  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwwisshclwwsn  29952  clwwlknon1nloop  30035  eucrctshift  30179  eucrct2eupth  30181  unopbd  31951  nmopcoi  32031  resvsca  33311  resvlem  33312  satfv1lem  35356  bj-prmoore  37110  ax12indalem  38945  afvres  47177  afvco2  47181  2ffzoeq  47332  difmodm1lt  47364  ply1mulgsumlem2  48380  lcoel0  48421  lindslinindsimp1  48450  digexp  48600  dig1  48601  itsclc0yqsol  48757