Theorem 3com13 1262

Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com13	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem 3com13

Step	Hyp	Ref	Expression
1		3anrev 1042	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 206	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1031

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  3coml  1264  3adant3l  1314  3adant3r  1315  syld3an1  1364  oacan  7515  oaword1  7519  nnacan  7595  nnaword1  7596  elmapg  7757  fisseneq  8056  ltapr  9746  subadd  10163  ltaddsub  10381  leaddsub  10383  iooshf  12123  faclbnd4  12946  relexpsucr  13617  relexpsucl  13621  dvdsmulc  14847  lcmdvdsb  15164  infpnlem1  15452  fmf  21559  frgra3v  26529  nvs  26902  dipdi  27082  dipsubdi  27088  spansncol  27811  chirredlem2  28634  mdsymlem3  28648  isbasisrelowllem2  32380  ltflcei  32567  iscringd  32967  iunrelexp0  37013  uun123p4  38060  isosctrlem1ALT  38192  stoweidlem17  38910  frgr3v  41445