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  4286  noel  4331  noelOLD  4332  axnulALT  5304  axnul  5305  cnv0  6145  imadif  6637  poxp3  8155  xrltnr  13132  nltmnf  13142  0nelfz1  13553  smu01  16461  3lcm2e6woprm  16586  6lcm4e12  16587  join0  18397  meet0  18398  nsmndex1  18865  smndex2dnrinv  18867  zringndrg  21394  zclmncvs  25089  nolt02o  27641  nogt01o  27642  legso  28416  rgrx0ndm  29420  wwlksnext  29717  ntrl2v2e  29981  avril1  30286  helloworld  30288  topnfbey  30292  xrge00  32755  fmlaomn0  35000  gonan0  35002  goaln0  35003  prv0  35040  dfon2lem7  35385  nandsym1  35906  bj-inftyexpitaudisj  36684  padd01  39284  ifpdfan  42896  sucomisnotcard  42974  clsk1indlem4  43474  iblempty  45353  salexct2  45727  0nodd  47232  2nodd  47234  1neven  47300  ipolub00  48004