Theorem 3com12 839

Description: Commutation in antecedent. Swap 1st and 3rd.

Hypothesis

Ref	Expression
3exp.1	⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Assertion

Ref	Expression
3com12	⊢ ((ψ ⋀ φ ⋀ χ) → θ)

Proof of Theorem 3com12

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 ⊢ ((φ ⋀ ψ ⋀ χ) → θ)
2	1	3exp 834	. . 3 ⊢ (φ → (ψ → (χ → θ)))
3	2	com12 11	. 2 ⊢ (ψ → (φ → (χ → θ)))
4	3	3imp 829	1 ⊢ ((ψ ⋀ φ ⋀ χ) → θ)

Syntax hints:   → wi 3   ⋀ w3a 777

This theorem is referenced by:  3adant2l 856  3adant2r 857  relelrng 3353  ecopoprtrn 4317  add12t 5348  addsubt 5396  mul12t 5430  ppncant 5493  ltaddsub2t 5644  leaddsub2t 5646  lesub2t 5673  ltsub2t 5675  div23t 5749  divdivdivt 5787  ltmulgt11t 5848  lediv1t 5853  lediv1tOLD 5854  ltmuldiv2tOLD 5868  ltdivmultOLD 5870  ledivmultOLD 5871  lt2mul2divt 5874  lemuldivt 5876  lemuldivtOLD 5877  lemuldiv2tOLD 5879  ltdiv2t 5889  nndivt 5961  ioonegt 6407  icoshft 6409  fznn0subt 6499  fzaddelt 6501  fzshftralt 6523  abssubge0t 6895  facwordit 6944  bccl2t 6971  fsummulc2 7034  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  cvgcmp3c 7186  efaddlem24 7361  znnenlem 7502  2basgent 7640  ioo2bl 7909  tgioolem 7911  xplm 7972  isgrp2i 8072  vcdi 8167  isvci 8197  ipdi 8499  ipsubdi 8505  hvadd12t 8899  hvmulcomt 8907  his5t 8948  bcs3t 9045  chj12t 9452  homul12t 9726  hoaddsubt 9737  kbmult 9874  lnopmult 9886  lnopaddmul 9892  lnopsubmul 9894  homco2t 9896  lnfnaddmul 9969  leop2t 10052  dmdsl3t 10237  irredlem3 10314  atmd2 10322  cdj3lem3 10360  nndivsub 10416  cnvhmph 10513  hmphsyma 10514

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain