Theorem 3com13 1270

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 1049	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 207	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3coml  1272  3adant3l  1322  3adant3r  1323  syld3an1  1372  oacan  7628  oaword1  7632  nnacan  7708  nnaword1  7709  elmapg  7870  fisseneq  8171  ltapr  9867  subadd  10284  ltaddsub  10502  leaddsub  10504  iooshf  12252  faclbnd4  13084  relexpsucr  13769  relexpsucl  13773  dvdsmulc  15009  lcmdvdsb  15326  infpnlem1  15614  fmf  21749  frgr3v  27139  nvs  27518  dipdi  27698  dipsubdi  27704  spansncol  28427  chirredlem2  29250  mdsymlem3  29264  isbasisrelowllem2  33204  ltflcei  33397  iscringd  33797  iunrelexp0  37994  uun123p4  39039  isosctrlem1ALT  39170  stoweidlem17  40234