Theorem intnan 486

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
intnan.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
intnan	⊢ ¬ (𝜓 ∧ 𝜑)

Proof of Theorem intnan

Step	Hyp	Ref	Expression
1		intnan.1	. 2 ⊢ ¬ 𝜑
2		simpr 484	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 196	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ 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 206  df-an 396

This theorem is referenced by:  bianfi  533  indifdirOLD  4216  noel  4261  noelOLD  4262  dfopif  4797  axnulALT  5223  axnul  5224  cnv0  6033  imadif  6502  xrltnr  12784  nltmnf  12794  0nelfz1  13204  smu01  16121  3lcm2e6woprm  16248  6lcm4e12  16249  join0  18038  meet0  18039  nsmndex1  18467  smndex2dnrinv  18469  zringndrg  20602  zclmncvs  24217  legso  26864  rgrx0ndm  27863  wwlksnext  28159  ntrl2v2e  28423  avril1  28728  helloworld  28730  topnfbey  28734  xrge00  31197  fmlaomn0  33252  gonan0  33254  goaln0  33255  prv0  33292  dfon2lem7  33671  poxp3  33723  nolt02o  33825  nogt01o  33826  nandsym1  34538  subsym1  34543  bj-inftyexpitaudisj  35303  padd01  37752  ifpdfan  40971  clsk1indlem4  41543  iblempty  43396  salexct2  43768  0nodd  45252  2nodd  45254  1neven  45378  ipolub00  46167