Theorem pm2.61ian 821

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  4cases  1051  cases2ALT  1059  consensus  1063  preqsnd  4814  csbexg  5257  snopeqop  5472  xpcan2  6158  tfindsg  7836  findsg  7873  ixpexg  8898  fipwss  9369  ranklim  9796  fin23lem14  10284  fzoval  13659  modsumfzodifsn  13951  hashge2el2dif  14487  iswrdi  14524  swrd0  14666  swrdsbslen  14672  swrdspsleq  14673  pfxccatin12  14740  swrdccat  14742  pfxccat3a  14745  repswswrd  14791  cshword  14798  cshwcsh2id  14835  dvdsabseq  16338  m1exp1  16401  flodddiv4  16440  dfgcd2  16571  lcmftp  16661  prmop1  17065  fvprmselelfz  17071  ressbas  17263  resseqnbas  17269  ressinbas  17272  cntzval  19352  symg2bas  19424  sralem  21231  srasca  21235  sravsca  21236  sraip  21237  ocvval  21707  dsmmval  21774  dmatmul  22545  1mavmul  22596  mavmul0g  22601  1marepvmarrepid  22623  smadiadetglem2  22720  1elcpmat  22763  decpmatid  22818  tnglem  24688  tngds  24696  gausslemma2dlem1a  27417  2lgslem1c  27445  2sqreulem1  27498  2sqreunnlem1  27501  nosupno  27755  nosupbday  27757  nosupbnd1lem5  27764  nosupbnd1  27766  nosupbnd2  27768  noinfno  27770  noinfbday  27772  noinfbnd1lem5  27779  noinfbnd1  27781  noinfbnd2  27783  madess  27947  abssge0  28326  clwlkclwwlklem2a4  30156  clwlkclwwlklem2a  30157  clwwisshclwwsn  30175  clwwlknon1nloop  30258  eucrctshift  30402  eucrct2eupth  30404  unopbd  32175  nmopcoi  32255  resvsca  33479  resvlem  33480  satfv1lem  35673  bj-prmoore  37566  ax12indalem  39530  afvres  47727  afvco2  47731  2ffzoeq  47883  difmodm1lt  47920  ply1mulgsumlem2  48970  lcoel0  49011  lindslinindsimp1  49040  digexp  49190  dig1  49191  itsclc0yqsol  49347