Theorem pm2.61ian 810

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

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

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 399

This theorem is referenced by:  4cases  1035  cases2ALT  1043  consensus  1047  preqsnd  4791  csbexg  5216  snopeqop  5398  xpcan2  6036  tfindsg  7577  findsg  7611  ixpexg  8488  fipwss  8895  ranklim  9275  fin23lem14  9757  fzoval  13042  modsumfzodifsn  13315  hashge2el2dif  13841  iswrdi  13868  ffz0iswrdOLD  13894  swrd0  14022  swrdsbslen  14028  swrdspsleq  14029  pfxccatin12  14097  swrdccat  14099  pfxccat3a  14102  repswswrd  14148  cshword  14155  cshwcsh2id  14192  dvdsabseq  15665  m1exp1  15729  flodddiv4  15766  dfgcd2  15896  lcmftp  15982  prmop1  16376  fvprmselelfz  16382  ressbas  16556  resslem  16559  ressinbas  16562  cntzval  18453  symg2bas  18523  sralem  19951  srasca  19955  sravsca  19956  sraip  19957  ocvval  20813  dsmmval  20880  dmatmul  21108  1mavmul  21159  mavmul0g  21164  1marepvmarrepid  21186  smadiadetglem2  21283  1elcpmat  21325  decpmatid  21380  tnglem  23251  tngds  23259  gausslemma2dlem1a  25943  2lgslem1c  25971  2sqreulem1  26024  2sqreunnlem1  26027  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  clwwisshclwwsn  27796  clwwlknon1nloop  27880  eucrctshift  28024  eucrct2eupth  28026  unopbd  29794  nmopcoi  29874  resvsca  30905  resvlem  30906  satfv1lem  32611  noprefixmo  33204  nosupno  33205  nosupbday  33207  nosupbnd1lem5  33214  nosupbnd1  33216  nosupbnd2  33218  bj-prmoore  34409  ax12indalem  36083  afvres  43378  afvco2  43382  2ffzoeq  43535  ply1mulgsumlem2  44448  lcoel0  44490  lindslinindsimp1  44519  difmodm1lt  44589  digexp  44674  dig1  44675  itsclc0yqsol  44758