Theorem imnani 423

Description: Infer implication from negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)

Hypothesis

Ref	Expression
imnani.1

Assertion

Ref	Expression
imnani

Proof of Theorem imnani

Step	Hyp	Ref	Expression
1		imnani.1	. 2
2		imnan 422	. 2
3	1, 2	mpbir 209	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369

This theorem is referenced by:  mptnan  1601  eueq3  3274  onuninsuci  6675  sucprcreg  8046  alephsucdom  8481  pwfseq  9063  eirr  13938  mreexmrid  15040  dvferm1  22386  dvferm2  22388  dchrisumn0  23706  rpvmasum  23711  cvnsym  27209  ballotlem2  28427  bnj1224  33860  bnj1541  33914  bnj1311  34080  bj-imn3ani  34176

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 185  df-an 371