Theorem impancom 258

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

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

Assertion

Ref	Expression
impancom	⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 114	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 123	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  eqrdav  2099  disjiun  3870  euotd  4114  onsucelsucr  4362  isotr  5649  spc2ed  6060  ltbtwnnqq  7124  genpcdl  7228  genpcuu  7229  un0addcl  8862  un0mulcl  8863  btwnnz  8997  uznfz  9724  elfz0ubfz0  9743  fzoss1  9789  elfzo0z  9802  fzofzim  9806  elfzom1p1elfzo  9832  ssfzo12bi  9843  subfzo0  9860  modfzo0difsn  10009  expaddzap  10178  caucvgre  10593  caubnd2  10729  summodc  10991  fzo0dvdseq  11350  nno  11398  lcmdvds  11553  hashgcdeq  11696  neii1  12098  neii2  12100