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 197	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 207  df-an 396

This theorem is referenced by:  bianfi  533  noel  4292  uni0  4893  axnulALT  5251  axnul  5252  cnv0  6105  cnv0OLD  6106  imadif  6584  poxp3  8102  1div0  11808  xrltnr  13045  nltmnf  13055  0nelfz1  13471  smu01  16425  3lcm2e6woprm  16554  6lcm4e12  16555  join0  18338  meet0  18339  nsmndex1  18850  smndex2dnrinv  18852  zringndrg  21435  zclmncvs  25116  nolt02o  27675  nogt01o  27676  legso  28683  rgrx0ndm  29679  wwlksnext  29978  ntrl2v2e  30245  avril1  30550  helloworld  30552  topnfbey  30556  xrge00  33107  axnulALT2  35258  axsepg2ALT  35260  fmlaomn0  35606  gonan0  35608  goaln0  35609  prv0  35646  dfon2lem7  36003  nandsym1  36638  bj-inftyexpitaudisj  37460  padd01  40187  ifpdfan  43822  sucomisnotcard  43900  clsk1indlem4  44400  iblempty  46323  salexct2  46697  0nodd  48530  2nodd  48532  1neven  48598  ipolub00  49352