![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > an42s | GIF version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an41r3s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
an42s | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an41r3s.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | an4s 588 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
3 | 2 | ancom2s 566 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: nnmsucr 6489 ecopoveq 6630 enqdc 7360 addcmpblnq 7366 addpipqqslem 7368 addpipqqs 7369 addclnq 7374 addcomnqg 7380 distrnqg 7386 recexnq 7389 ltdcnq 7396 ltexnqq 7407 enq0enq 7430 enq0sym 7431 enq0breq 7435 addclnq0 7450 distrnq0 7458 mulclsr 7753 axmulass 7872 axdistr 7873 subadd4 8201 mulsub 8358 mgmidmo 12791 tgcl 13567 |
Copyright terms: Public domain | W3C validator |