Theorem intnan 490

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 488	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 200	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  bianfi  537  indifdirOLD  4174  noel  4217  noelOLD  4218  dfopif  4752  axnulALT  5169  axnul  5170  cnv0  5967  imadif  6417  xrltnr  12590  nltmnf  12600  0nelfz1  13010  smu01  15922  3lcm2e6woprm  16049  6lcm4e12  16050  meet0  17856  join0  17857  nsmndex1  18187  smndex2dnrinv  18189  zringndrg  20302  zclmncvs  23893  legso  26537  rgrx0ndm  27527  wwlksnext  27823  ntrl2v2e  28087  avril1  28392  helloworld  28394  topnfbey  28398  xrge00  30864  fmlaomn0  32915  gonan0  32917  goaln0  32918  prv0  32955  dfon2lem7  33329  poxp3  33399  nolt02o  33531  nogt01o  33532  nandsym1  34241  subsym1  34246  bj-inftyexpitaudisj  34986  padd01  37437  ifpdfan  40611  clsk1indlem4  41184  iblempty  43032  salexct2  43404  0nodd  44882  2nodd  44884  1neven  45008