ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  an42s GIF version

Theorem an42s 531
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an41r3s.1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
an42s (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)

Proof of Theorem an42s
StepHypRef Expression
1 an41r3s.1 . . 3 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
21an4s 530 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 508 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  nnmsucr  6097  ecopoveq  6231  enqdc  6516  addcmpblnq  6522  addpipqqslem  6524  addpipqqs  6525  addclnq  6530  addcomnqg  6536  distrnqg  6542  recexnq  6545  ltdcnq  6552  ltexnqq  6563  enq0enq  6586  enq0sym  6587  enq0breq  6591  addclnq0  6606  distrnq0  6614  mulclsr  6896  axmulass  7004  axdistr  7005  subadd4  7317  mulsub  7469
  Copyright terms: Public domain W3C validator