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  4812  csbexg  5252  snopeqop  5451  xpcan2  6132  tfindsg  7800  findsg  7836  ixpexg  8856  fipwss  9324  ranklim  9748  fin23lem14  10235  fzoval  13567  modsumfzodifsn  13858  hashge2el2dif  14394  iswrdi  14431  swrd0  14573  swrdsbslen  14579  swrdspsleq  14580  pfxccatin12  14647  swrdccat  14649  pfxccat3a  14652  repswswrd  14698  cshword  14705  cshwcsh2id  14742  dvdsabseq  16231  m1exp1  16294  flodddiv4  16333  dfgcd2  16464  lcmftp  16554  prmop1  16957  fvprmselelfz  16963  ressbas  17154  resseqnbas  17160  ressinbas  17163  cntzval  19241  symg2bas  19313  sralem  21119  srasca  21123  sravsca  21124  sraip  21125  ocvval  21613  dsmmval  21680  dmatmul  22432  1mavmul  22483  mavmul0g  22488  1marepvmarrepid  22510  smadiadetglem2  22607  1elcpmat  22650  decpmatid  22705  tnglem  24575  tngds  24583  gausslemma2dlem1a  27323  2lgslem1c  27351  2sqreulem1  27404  2sqreunnlem1  27407  nosupno  27662  nosupbday  27664  nosupbnd1lem5  27671  nosupbnd1  27673  nosupbnd2  27675  noinfno  27677  noinfbday  27679  noinfbnd1lem5  27686  noinfbnd1  27688  noinfbnd2  27690  madess  27841  abssge0  28203  clwlkclwwlklem2a4  29998  clwlkclwwlklem2a  29999  clwwisshclwwsn  30017  clwwlknon1nloop  30100  eucrctshift  30244  eucrct2eupth  30246  unopbd  32016  nmopcoi  32096  resvsca  33341  resvlem  33342  satfv1lem  35478  bj-prmoore  37232  ax12indalem  39117  afvres  47334  afvco2  47338  2ffzoeq  47489  difmodm1lt  47521  ply1mulgsumlem2  48549  lcoel0  48590  lindslinindsimp1  48619  digexp  48769  dig1  48770  itsclc0yqsol  48926