Theorem simpli 111

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpli	⊢ 𝜑

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-ia1 106

This theorem is referenced by:  biimp  118  biimpr  130  dfbi2  392  orc  724  pwundifss  4428  ssdomg  7059  negiso  9279  infrenegsupex  9977  xrnegiso  12011  infxrnegsupex  12012  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  sin4lt0  12517  egt2lt3  12530  epos  12531  ene1  12535  eap1  12536  slotslfn  13361  strslfvd  13377  strslfv2d  13378  strsl0  13384  setsslid  13386  setsslnid  13387  slotm  13398  sravscag  14763  reeff1o  15857  pigt2lt4  15868  pire  15870  pipos  15872  sinhalfpi  15880  tan4thpi  15925  sincos3rdpi  15927  pigt3  15928  lgsdir2lem4  16133  lgsdir2lem5  16134