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

Theorem an42s 578
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 577 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 555 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nnmsucr  6384  ecopoveq  6524  enqdc  7176  addcmpblnq  7182  addpipqqslem  7184  addpipqqs  7185  addclnq  7190  addcomnqg  7196  distrnqg  7202  recexnq  7205  ltdcnq  7212  ltexnqq  7223  enq0enq  7246  enq0sym  7247  enq0breq  7251  addclnq0  7266  distrnq0  7274  mulclsr  7569  axmulass  7688  axdistr  7689  subadd4  8013  mulsub  8170  tgcl  12243
  Copyright terms: Public domain W3C validator