Theorem pm2.61ian 812

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  1041  cases2ALT  1049  consensus  1053  preqsnd  4803  csbexg  5245  snopeqop  5454  xpcan2  6135  tfindsg  7805  findsg  7841  ixpexg  8863  fipwss  9335  ranklim  9759  fin23lem14  10246  fzoval  13605  modsumfzodifsn  13897  hashge2el2dif  14433  iswrdi  14470  swrd0  14612  swrdsbslen  14618  swrdspsleq  14619  pfxccatin12  14686  swrdccat  14688  pfxccat3a  14691  repswswrd  14737  cshword  14744  cshwcsh2id  14781  dvdsabseq  16273  m1exp1  16336  flodddiv4  16375  dfgcd2  16506  lcmftp  16596  prmop1  17000  fvprmselelfz  17006  ressbas  17197  resseqnbas  17203  ressinbas  17206  cntzval  19287  symg2bas  19359  sralem  21163  srasca  21167  sravsca  21168  sraip  21169  ocvval  21657  dsmmval  21724  dmatmul  22472  1mavmul  22523  mavmul0g  22528  1marepvmarrepid  22550  smadiadetglem2  22647  1elcpmat  22690  decpmatid  22745  tnglem  24615  tngds  24623  gausslemma2dlem1a  27342  2lgslem1c  27370  2sqreulem1  27423  2sqreunnlem1  27426  nosupno  27681  nosupbday  27683  nosupbnd1lem5  27690  nosupbnd1  27692  nosupbnd2  27694  noinfno  27696  noinfbday  27698  noinfbnd1lem5  27705  noinfbnd1  27707  noinfbnd2  27709  madess  27872  abssge0  28251  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwwisshclwwsn  30101  clwwlknon1nloop  30184  eucrctshift  30328  eucrct2eupth  30330  unopbd  32101  nmopcoi  32181  resvsca  33407  resvlem  33408  satfv1lem  35560  bj-prmoore  37443  ax12indalem  39405  afvres  47632  afvco2  47636  2ffzoeq  47788  difmodm1lt  47825  ply1mulgsumlem2  48875  lcoel0  48916  lindslinindsimp1  48945  digexp  49095  dig1  49096  itsclc0yqsol  49252