Theorem pm2.61ian 823

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

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

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 210  df-an 401

This theorem is referenced by:  4cases  1056  cases2ALT  1064  consensus  1068  preqsnd  4825  csbexg  5274  snopeqop  5491  xpcan2  6177  tfindsg  7858  findsg  7895  ixpexg  8921  fipwss  9390  ranklim  9817  fin23lem14  10318  fzoval  13690  modsumfzodifsn  13982  hashge2el2dif  14519  iswrdi  14556  swrd0  14698  swrdsbslen  14704  swrdspsleq  14705  pfxccatin12  14772  swrdccat  14774  pfxccat3a  14777  repswswrd  14823  cshword  14830  cshwcsh2id  14867  dvdsabseq  16372  m1exp1  16435  flodddiv4  16474  dfgcd2  16605  lcmftp  16695  prmop1  17099  fvprmselelfz  17105  ressbas  17297  resseqnbas  17303  ressinbas  17306  cntzval  19392  symg2bas  19464  sralem  21278  srasca  21282  sravsca  21283  sraip  21284  isfieldidl  21367  ocvval  21798  dsmmval  21865  dmatmul  22635  1mavmul  22686  mavmul0g  22691  1marepvmarrepid  22713  smadiadetglem2  22810  1elcpmat  22853  decpmatid  22908  tnglem  24778  tngds  24786  gausslemma2dlem1a  27510  2lgslem1c  27538  2sqreulem1  27591  2sqreunnlem1  27594  nosupno  27848  nosupbday  27850  nosupbnd1lem5  27857  nosupbnd1  27859  nosupbnd2  27861  noinfno  27863  noinfbday  27865  noinfbnd1lem5  27872  noinfbnd1  27874  noinfbnd2  27876  madess  28040  abssge0  28419  clwlkclwwlklem2a4  30329  clwlkclwwlklem2a  30330  clwwisshclwwsn  30348  clwwlknon1nloop  30431  eucrctshift  30575  eucrct2eupth  30577  unopbd  32348  nmopcoi  32428  resvsca  33633  resvlem  33634  satfv1lem  35835  bj-prmoore  37738  ax12indalem  39700  afvres  47892  afvco2  47896  2ffzoeq  48048  difmodm1lt  48085  ply1mulgsumlem2  49150  lcoel0  49191  lindslinindsimp1  49220  digexp  49370  dig1  49371  itsclc0yqsol  49527