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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  eqrdav  2164  disjiun  3977  euotd  4232  onsucelsucr  4485  isotr  5784  spc2ed  6201  ltbtwnnqq  7356  genpcdl  7460  genpcuu  7461  un0addcl  9147  un0mulcl  9148  btwnnz  9285  uznfz  10038  elfz0ubfz0  10060  fzoss1  10106  elfzo0z  10119  fzofzim  10123  elfzom1p1elfzo  10149  ssfzo12bi  10160  subfzo0  10177  modfzo0difsn  10330  expaddzap  10499  caucvgre  10923  caubnd2  11059  summodc  11324  fzo0dvdseq  11795  nno  11843  lcmdvds  12011  hashgcdeq  12171  modprm0  12186  pcqcl  12238  neii1  12797  neii2  12799  fsumcncntop  13206