Theorem pm2.61ian 824

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  4cases  1056  cases2ALT  1064  consensus  1068  preqsnd  4819  csbexg  5270  snopeqop  5485  xpcan2  6187  tfindsg  7906  findsg  7943  ixpexg  8988  fipwss  9458  ranklim  9895  fin23lem14  10450  fzoval  13834  modsumfzodifsn  14127  hashge2el2dif  14666  iswrdi  14703  swrd0  14850  swrdsbslen  14856  swrdspsleq  14857  pfxccatin12  14924  swrdccat  14926  pfxccat3a  14929  repswswrd  14977  cshword  14984  cshwcsh2id  15021  dvdsabseq  16527  m1exp1  16590  flodddiv4  16629  dfgcd2  16763  lcmftp  16855  prmop1  17260  fvprmselelfz  17266  ressbas  17458  resseqnbas  17464  ressinbas  17467  cntzval  19586  symg2bas  19658  sralem  21502  srasca  21506  sravsca  21507  sraip  21508  isfieldidl  21591  ocvval  22028  dsmmval  22095  dmatmul  22867  1mavmul  22918  mavmul0g  22923  1marepvmarrepid  22945  smadiadetglem2  23042  1elcpmat  23088  decpmatid  23143  tnglem  25014  tngds  25022  gausslemma2dlem1a  27749  2lgslem1c  27777  2sqreulem1  27830  2sqreunnlem1  27833  nosupno  28117  nosupbday  28119  nosupbnd1lem5  28126  nosupbnd1  28128  nosupbnd2  28130  noinfno  28132  noinfbday  28134  noinfbnd1lem5  28141  noinfbnd1  28143  noinfbnd2  28145  madess  28309  abssge0  28688  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwwisshclwwsn  30664  clwwlknon1nloop  30747  eucrctshift  30901  eucrct2eupth  30903  unopbd  32674  nmopcoi  32754  resvsca  33997  resvlem  33998  acwer1prclem  35892  satfv1lem  36335  bj-prmoore  38306  ax12indalem  40268  afvres  48515  afvco2  48519  2ffzoeq  48671  difmodm1lt  48708  ply1mulgsumlem2  49830  lcoel0  49871  lindslinindsimp1  49900  digexp  50050  dig1  50051  itsclc0yqsol  50207