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

Theorem an42s 523
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 522 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 500 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nnmsucr  6054  ecopoveq  6188  enqdc  6440  addcmpblnq  6446  addpipqqslem  6448  addpipqqs  6449  addclnq  6454  addcomnqg  6460  distrnqg  6466  recexnq  6469  ltdcnq  6476  ltexnqq  6487  enq0enq  6510  enq0sym  6511  enq0breq  6515  addclnq0  6530  distrnq0  6538  mulclsr  6820  axmulass  6928  axdistr  6929  subadd4  7234  mulsub  7377
  Copyright terms: Public domain W3C validator